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, 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