Automated Theorem Proving

Contents

• Introduction
• Examples relating Logic to Mathematics and Computer Science
• Simple law text.
• Sorting by pattern matching.
• Pattern based matching using Mathematica: GCD, Sum, Sorting: Mathematica programs. The relationship between logic and programming, see also reverse.pdf
• Termination of programs.
• The role of Mathematics and Logic in science.
• Intelectual problem solving: observe - solve - apply.
• The role of Mathematics and of Mathematical Logic and their importance.
• The intelectual problem solving cycle in our profesion, the role computer and of automated reasoning.
• Applications of logic: verification of systems, semantic web.
• Propositional Logic
• Syntax.
• The main parts of a logic model: syntax, semantics, pragmatics.
• The definition of syntax as a language: alphabet, composition rules.
• The inductive principle in the definition of syntax and its applications: defining functions, proving statements.
• Semantics, Semantics based notions.
• The main principle of semantics: interpretations, truth value, truth valuation function.
• The truth table.
• Semantics based notions: validity, consistency, semantical logical consequence, semantic equivalence.
• Proving semantical logical consequence by validity of implication.
• Semantic equivalence as validity of syntactical equivalence, and as double semantic consequence.
• Proving semantical logical consequence by refutation.
• Using the truth table for proving: validity, semantical equivalence, semantical logical consequence.
• Rewriting to Normal Form
• The use of semantic equivalence for rewriting formulae.
• Using equivalences for transforming formulae: Negation Normal Form, Conjunctive Normal Form, Disjunctive Normal Form.
• Demo transformation in Negation Normal Form demo-NNF.pdf (use a pdf reader and full screen landscape mode). The program in C which constructs the tree of a formula and transforms it into NNF, also producing the previous demo treeProving.c.pdf
• Proving equivalences by reduction to CNF - incompleteness.
• Proving validity by reduction to CNF - completeness.
• Syntax and Semantics Revisited
• Some basic properties of conjunction and disjunction: idempotence, commutativity, associativity.
• Embedding these properties at syntactic level by considering conjunctive and disjunctive sets Conjunctive-Disjunctive-Sets_19-Apr-2020.pdf.
• Resolution in Propositional Logic
• The resolution principle: the inference rule, the proof method.
• Correctness of the proof method.
• Completeness of resolution for propositional logic.
• Resolution experiments Resolution-Experiments-presentation.pdf.
• Unit resolution and unit subsumption.
• The Davis-Putnam-Logemann-Loveland (DPLL) algorithm.
• The Chaff techinque for eficient implementation of DPLL Chaff.pdf

• Sequent Calculus in Propositional Logic

• First Order Predicate Logic:

• Programming as a Logical Paradigm: