## 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. |

### What people are saying - Write a review

#### Review: Logic (Trinity Paper, #9)

User Review - Carlos E. Montijo - GoodreadsThe best book on logic that I know of. Read full review

#### Review: Logic (Trinity Paper, #9)

User Review - Leah - GoodreadsHard for me to follow his A/B/C/D diagrams and seemed a little long winded. Finally caught on to what he was saying in the last few chapters. Short, though, but dense. Read full review

### Contents

Syntax and Intuitive Semantics | 8 |

Boolean Analysis of Sentences | 35 |

Infinite Finitary Trees and Boolean Compactness | 61 |

Copyright | |

10 other sections not shown

### Common terms and phrases

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