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
already applied argument axiom Boolean valuation branch calculus called choice clausal sequent clause closed complete components computation condition conjunction CONS consider construction contains corresponding deduction defined definition denote determined disjunction empty equation v(X equations equivalent example expression fact false falsifies finite formulas function give given hence Herbrand idea immediate constituents individual inference infinite instance labelled least length LISP logical logical model means namely node normal notation Note notion occur operator pair possible predicate premisses procedure proof prove pure quantifiers QUOTE reasoning replace represented resolution resolvent result returns rule satisfies selected semantic sentence sequent shows side simply space step substitution successor Suppose symbol tableau term tree true truth truthvalues unifier universe variables write yields