Logic, Form and Function: The Mechanization of Deductive Reasoning
Logic: 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.
35 pages matching variant in this book
Results 1-3 of 35
What people are saying - Write a review
We haven't found any reviews in the usual places.
Syntax and Intuitive Semantics
Boolean Analysis of Sentences
Infinite Finitary Trees and Boolean Compactness
10 other sections not shown
Other editions - View all
3xQx applied arity Boolean constituents Boolean valuation called closed formulas closed sentences closed term components computation COND NULL 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 inference node infinite set input labelled lexicon Lisp machine logical model logically equivalent model of pure non-empty normal form normal proof procedure notation occur operator ordinal numbers pair PI-RESOLVE predicate calculus premisses prenex prenex normal form quantifiers RESLAB resolution resolution principle resolvent right clause S-expressions satisfies selection rule semantic tableau sentences of pure set of equations SETQ Skolem Skolem normal form step substitution SUBSUMES symbol true sequent truthvalues Unification Algorithm unifier universe variables variant