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