• Examples relating Logic to Mathematics and Computer Science
  • Simple law text.
  • Russel's paradox.
  • 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.

• 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
  • Sequents, proof trees, axioms, sequent rules as models of elements from natural-style proving Sequent-Calculus-04-May-2020.pdf.
  • Construction of a correct and complete calculus for formulae containing only negation and conjunction.
  • Example of natural-style proof which uses the rule for negation in the assumptions: proof-example.pdf.
  • Completeness and correctness of the "not-and" sequent calculus.
  • Extending the calculus to the other logical connectives.
  • Treatment of truth constants.
  • Special rules (modus ponens, subsumption, resolution, implied goal).
  • Unique goal sequent calculus.
  • Sequent calculus with unit propagation.
  • Automatically generated proofs in the Theorema system (for Mathematica notebooks you can use for free the Wolfram player: https://www.wolfram.com/player) using sequent calculus (Proof-abc1-classic.nb, Proof-abc1-classic.pdf, Proof-abc2-classic.nb, Proof-abc2-classic.pdf, Proof-invalid-classic.nb, Proof-invalid-classic.pdf), sequent calculus with unit propagation (Proof-abc1-propagation.nb, Proof-abc1-propagation.pdf, Proof-abc2-propagation.nb, Proof-abc2-propagation.pdf, Proof-invalid-propagation.nb, Proof-invalid-propagation.pdf).

• First Order Predicate Logic:
  • Syntax FOL-1-Syntax_19-May-2020.
  • Semantics FOL-2-Semantics_19-May-2020.pdf.
  • Rewriting by equivalence and normal forms: prenex, Skolem, standard FOL-3-Normal-Forms_21-May-2020.
  • Substitutions, unification FOL-4-Resolution_23-Jun-2020.
  • Resolution in first order predicate logic, correctness.
  • Sequent calculus in predicate logic FOL-5-Sequent-Calculus_23-Jun-2020.
  • Predicate logic with equality, computation by substitution and replacement FOL-6-Equality_5-Jun-2020.

• Reasoning about programs, transformation into tail-recursive form reverse.pdf.
• Program verification paper and presentation.

Additional Material

Lecture notes: Introduction-to-ATP-Jebelean-5-Jun-2018.pdf.

Suggested exercises: exercises.pdf.

The contents of the lecture is very similar to the transcript by Martin Koehler of previous lectures: pdf file. (May contain some typos and small errors.)

For more details (some of which are not covered in the lecture) I recommend: Bruno Buchberger: Logic for Computer Science pdf file. This material is copyrighted and is available only for the students of this lecture and only for the purpose of study related to it.

The home pages of the similar lectures in Linz: Mathematical Logic, Computational Logic.