What people are saying - Write a review
We haven't found any reviews in the usual places.
Resolution and logic programming
7 other sections not shown
3-formula 3-rules algorithm applied arbitrary assignment Assumption atoms Axiom Boolean called clausal form closed completeness computer science conjunction constant construction decision procedure defined Definition denoted disjunction domain elements equations equivalent example exercise existential quantifiers F F F F T F failure node false finite formal formation tree free variables function symbols Gentzen system goal clause ground clauses Herbrand base Herbrand universe Hilbert system Hintikka set Hintikka structure infinite instantiation integers interpretation label Lemma logic programming mathematical logic negation notation occur check operators post-condition pre-condition predicate calculus programming language Prolog proof propositional calculus propositional letters provable Prove Theorem refutation resolution resolvent rule of inference schema semantic tableau semantic tree sequence set of clauses set of formulas set of literals statement subformula subset temporal logic terminate theory transformed true unifier universally quantified unsatisfiable valid formula VxA(x Vxg(x Vxp(x wp(S