Algebraic specification of data structures. Equational logic: validity and implication of equations, the system of equational rules. Reporting systems. Termination, Church-Rosser property, normal forms. The method of finite sub-terms. Minimal equation model. Unprovable equations. Propositions not expressible by equations. Completeness theorem of equation rules.
Prepositional phrases. The Gentzen system and top-down research. Refutation of propositional formulas by the method of resolution. Completeness theorems for the Gentzen system and for the solution. First class types. Gentzen’s general system and top-down general research. Completeness and compactness theorems. Propositions not expressible by first-order formulas. Introduction to logic programming. Consolidation of Terms. Solving universal formulas. Introduction to symbolic inductive proofs. Critical pairs of reference systems. The Knuth-Bendix method.