Automated model building

zbMath1085.03009MaRDI QIDQ2487870

Ricardo Caferra, Nicolas Peltier, Alexander Leitsch

Publication date: 11 August 2005

Published in: Applied Logic Series (Search for Journal in Brave)

zbMATH Keywords

Herbrand modelsautomated theorem provingautomated model buildingresolution-based methods

Mathematics Subject Classification ID

Related Items (18)

Semantically-guided goal-sensitive reasoning: model representation ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ MACE4 and SEM: A Comparison of Finite Model Generators ⋮ A Resolution-based Model Building Algorithm for a Fragment of OCC1N = ⋮ A superposition calculus for abductive reasoning ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ Decidability Results for Saturation-Based Model Building ⋮ Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas ⋮ 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 ⋮ Detecting Unknots via Equational Reasoning, I: Exploration ⋮ Theory decision by decomposition ⋮ Constructing infinite models represented by tree automata ⋮ Automated Model Building: From Finite to Infinite Models ⋮ SGGS decision procedures ⋮ Finite reasons for safety

This page was built for publication: Automated model building