What people are saying - Write a review
We haven't found any reviews in the usual places.
Parti PREDICATE LOGIC
Semantics of Predicate Logic
19 other sections not shown
admissible algorithm answer substitution application arbitrary Assume axiom system called Cardinal Chapter clauses closed formula computed congruence relation conservative extension consider consists contains correct specification critical pair data type defined Definition denoted derivation dom(A domain element empty equivalent example Exercise finite set free variables function symbol goal ground atoms ground terms Hence Herbrand model Hoare logic Hoare's calculus homomorphism Horn logic implies infinite interpretation isomorphic Lemma LK-derivation logic program logic with equality mergesort model of Ax module natural numbers node noetherian normal form obtain parameter partial correctness assertion path possess a model predicate logic predicate symbol prenex normal form procedure environment program formulas Prolog prove quantifiers queue rule semantics sequence sequent calculus set of equations signature Skolem normal form SLD-derivation SLD-refutation SLD-tree sort sorted(L string structural induction subset subterm succ Theorem tion trivial unifier valid verification Z-algebra Z-formula Z-terms