A calculus combining resolution and enumeration for building finite models
From MaRDI portal
Publication:1404976
DOI10.1016/S0747-7171(03)00027-0zbMath1019.03009MaRDI QIDQ1404976
Publication date: 25 August 2003
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Representing and building models for decidable subclasses of equational clausal logic ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ Blocking and other enhancements for bottom-up model generation methods
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- A method for simultaneous search for refutations and models by equational constraint solving
- Resolution methods for the decision problem
- Increasing model building capabilities by constraint solving on terms with integer exponents
- Proving Theorems with the Modification Method
- A new method for automated finite model building exploiting failures and symmetries
- A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
- Decision procedures and model building in equational clause logic
- Hyperresolution and automated model building
- A method for building models automatically. Experiments with an extension of OTTER
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
This page was built for publication: A calculus combining resolution and enumeration for building finite models
