Logic, Form and Function: The Mechanization of Deductive ReasoningLogic: form and content; Formulas: syntax and intuitive semantics; Boolean analysis of sentences; Infinitive finitary trees and boolean compactness; Semantic analysis of sentences and terms; Logical consequence: sequents and proofs; Logical equivalence: substitutivity and variants; Normal forms of sentences and sequents; Herbrand models and maps; Quad notation for clausal sequents; Unification; Resolution; Resolution on the computer; Historical notes; Appedix; Index. |
Contents
Syntax and Intuitive Semantics | 8 |
Boolean Analysis of Sentences | 35 |
Infinite Finitary Trees and Boolean Compactness | 61 |
Copyright | |
10 other sections not shown
Other editions - View all
Common terms and phrases
3xAx 3xBx 3xQx applied arity axiom B₁ Boolean constituents Boolean valuation C₁ called closed sentences closed term components computation conjunction construction contains the equation deduction denotation map disjunction empty left-hand side equation v(X example exemplification existential existential clause expression false falsifies finitary tree finite clausal sequent function given ground instance Herbrand base Herbrand map tree Herbrand universe HYPER-RESOLVE immediate constituents individual infinite set input König's Lemma labelled lexicon LISP machine logical model logically equivalent model of pure non-empty normal form normal proof procedure notation occur ordinal numbers P1-RESOLVE pair predicate calculus premisses prenex prenex normal form quantifiers RESLAB resolution resolution principle resolvent right clause S-expressions satisfies semantic tableau set of sentences SETQ Skolem Skolem normal form substitution SUBSUMES symbol true sequent truthvalues unifier universe variables variant Vx(Ax w₁ X₁ Y₁