Propositional ResolutionExplores completeness in propositional logic, resolution on clauses, conjunctive form, unit resolution, SAT solvers, and proof generation.
Theorem Proving and VampireExplores theorem proving in first-order logic and the saturation-based approach, highlighting the Vampire theorem prover.
Propositional Logic: Normal FormsExplores Disjunctive Normal Form and Conjunctive Normal Form in propositional logic, showing how to construct them and discussing their complexity.
Mathgraph Theorem ProverIntroduces the Mathgraph Theorem Prover, showcasing its unique approach to representing propositions and organizing graphs for first-order logic.
Second Order Logic: WS1S and HOLExplores Second Order Logic, WS1S, HOL, decision procedures, atomic and composite formulas, and the combination of WS1S with MONA in HOL.
