Automated model building
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.
- Theory decision by decomposition
- Constructing infinite models represented by tree automata
- Automated modelling of physical systems
- A superposition calculus for abductive reasoning
- SGGS decision procedures
- Blocking and other enhancements for bottom-up model generation methods
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- A complete and terminating approach to linear integer solving
- Finite reasons for safety. Parameterized verification by finite model finding
- Model generation for natural language interpretation and analysis.
- Semantically-guided goal-sensitive reasoning: model representation
- Satisfiability solving and model generation for quantified first-order logic formulas
- On deciding satisfiability by theorem proving with speculative inferences
- scientific article; zbMATH DE number 1507182 (Why is no real title available?)
- scientific article; zbMATH DE number 1748573 (Why is no real title available?)
- Hyperresolution and automated model building
- MACE4 and SEM: a comparison of finite model generators
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- Decidability Results for Saturation-Based Model Building
- A method for building models automatically. Experiments with an extension of OTTER
- Detecting Unknots via Equational Reasoning, I: Exploration
- Automated Model Building: From Finite to Infinite Models
- Mechanizing Mathematical Reasoning
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- Decision procedures using model building techniques
- Semigroups, keis and groups induced by knot diagrams: an experimental investigation with automated reasoning
- Automated deduction
- First-order automatic literal model generation
This page was built for publication: Automated model building
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2487870)
