Logic and Proof MT24, All the algorithms
This is a list of all the (examinable) algorithms presented in [[Course - Logic and Proof MT24]]U. Mainly so that I can see which algorithms I’ve covered in my notes.
- SAT for Horn formulas
- [[Notes - Logic and Proof MT24, Horn formulas]]U
- Description
- Proof
- Example
- SAT for 2CNF formulas
- [[Notes - Logic and Proof MT24, 2-CNF formulas]]U
- Description
- Proof
- Example
- Walk-SAT
- [[Notes - Logic and Proof MT24, Walk-SAT]]U
- Description
- Proof
- Example
- XOR SAT
- [[Notes - Logic and Proof MT24, XOR-Clauses]]U
- Description
- Proof
- Example
- Propositional resolution
- [[Notes - Logic and Proof MT24, Propositional resolution]]U
- Description
- Proof
- Example
- Interpolants from straight line programs
- [[Notes - Logic and Proof MT24, Interpolants]]U
- Description
- Proof
- Example
- Cutting planes
- [[Notes - Logic and Proof MT24, Cutting planes]]U
- Description
- Proof
- Example
- Cutting planes proofs from resolution
- [[Notes - Logic and Proof MT24, Cutting planes]]U
- Description
- Proof
- Example
- Interpolants from cutting planes (not even mentioned in notes yet)
- [[Notes - Logic and Proof MT24, Cutting planes]]U
- Description
- Proof
- Example
- Quantifier elimination
- [[Notes - Logic and Proof MT24, Quantifier elimination]]U
- Description
- Proof
- Example
- Quantifier elimination for unbounded dense linear orders
- [[Notes - Logic and Proof MT24, Unbounded dense linear orders]]U
- Description
- Proof
- Example
- Quantifier elimination for ordered divisible abelian groups
- [[Notes - Logic and Proof MT24, Ordered divisible abelian groups]]U
- Description
- Proof
- Example
- Quantifier elimination for the rado graph
- [[Notes - Logic and Proof MT24, Rado graph]]U
- Description
- Proof
- Example
- Quantifier elimination for algebraically closed fields
- [[Notes - Logic and Proof MT24, Algebraically closed fields]]U
- Description
- Proof
- Example
- Deciding Presburger arithmetic
- [[Notes - Logic and Proof MT24, Presburger arithmetic]]U
- Description
- Proof
- Example
- Skolemization
- [[Notes - Logic and Proof MT24, Skolemization]]U
- Description
- Proof
- Example
- First-order refutation with Herbrand’s theorem
- [[Notes - Logic and Proof MT24, Herbrand’s theorem]]U
- Description
- Proof
- Example
- Ground resolution
- [[Notes - Logic and Proof MT24, Ground resolution]]U
- Description
- Proof
- Example
- Martelli and Montanari’s algorithm
- [[Notes - Logic and Proof MT24, Unification and resolution]]U
- Description
- Proof
- Example
- Robinson’s algorithm
- [[Notes - Logic and Proof MT24, Unification and resolution]]U
- Description
- Proof
- Example
- First-order resolution
- [[Notes - Logic and Proof MT24, Unification and resolution]]U
- Description
- Proof (refutation completeness is non-examinable)
- Example