Handbook of Practical Logic and Automated Reasoning
This book meets the demand for a self-contained and broad-based account of the concepts, the machinery and the use of automated reasoning. The mathematical logic foundations are described in conjunction with practical application, all with the minimum of prerequisites. The approach is constructive, concrete and algorithmic: a key feature is that methods are described with reference to actual implementations (for which code is supplied) that readers can use, modify and experiment with. This book is ideally suited for those seeking a one-stop source for the general area of automated reasoning. It can be used as a reference, or as a place to learn the fundamentals, either in conjunction with advanced courses or for self study.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
algebra algorithm And(p,q apply arithmetic atomic formulas automated automated theorem proving axioms binary bool canonical case-split clauses coefﬁcients congruence conjunction consider critical pairs deﬁnable deﬁne deﬁnition disjunction domain equality equations eval example existential quantiﬁer exists failwith false ﬁelds ﬁnal ﬁnd ﬁnite ﬁrst ﬁrst-order logic fol formula forall free variables function symbols ground instances Herbrand holds Horn clauses hypothesis imp_trans implementation induction inﬁnite input instantiation integer integral domains interpretation itlist language Lemma let rec literals map fun match fm mathematical MESON monomial multiplication negation OCaml paramodulation polynomial predicate Presburger arithmetic problem programming proof propositional logic quantiﬁer quantiﬁer elimination quantiﬁer-free recursive refutation resolution result rewrite satisﬁable simple Skolem Skolem functions subst subterm tautology termval theorem proving theory transformation trivial true uniﬁcation uniﬁer unsatisﬁable valid valuation zero