Automated model building
From MaRDI portal
Publication:2487870
zbMath1085.03009MaRDI QIDQ2487870
Ricardo Caferra, Nicolas Peltier, Alexander Leitsch
Publication date: 11 August 2005
Published in: Applied Logic Series (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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