Automated model building (Q2487870)

The book focuses on deduction-based symbolic methods for construction of Herbrand models developed in the last years. As the set of satisfiable first-order formulae is not recursively enumerable, there can be no ``universal'' model building procedure. Proving theorems and constructing (counter-) models for theories are activities which lie at very heart of mathematics and even of science in general. Counterexamples serve the purpose to convince everybody of the necessity of each hypothesis in the statement of a theorem. One major goal of counterexamples is their irreplaceable role in the correction of wrong intuitions or in testing conjectures. This capability is needed for a deep understanding of proofs and is missing in present-day theorem provers. Besides serving as counterexamples, models play an important role in inference itself: they allow introducing semantics into a basically syntactic process. Theorem provers were mainly understood as inference engines producing proofs for provable sentences. The problem of dealing with nonderivable sentences received considerable less attention. The next step of the development of inference systems can be defined as that of model construction. It is the main purpose of this book to present and analyze such inference systems and to demonstrate their value to theorem proving and to science in general. In the same sense that proofs are more than just provability, models are more than the fact of satisfiability. Indeed, both proofs and models provide evidence, i.e., they show why statements hold or not. This underlies the conceptual value of model construction in general. The authors present traditional resolution provers as decision procedures, where model building takes place as a postprocessing procedure. They present new versions of the hyperresolution method and their extension to equational clause logic. The model building procedures are based on deduction closure and unit selection and do not require any form of backtracking. A second approach to symbolic model building is presented, and it is the constraint-based one. The authors demonstrate that constraint-based logics are not only useful to inference but are equally valuable in defining disinference rules, i.e., rules characterizing instances that cannot be inferred from given premises.