Extracting models from clause sets saturated under semantic refinements of the resolution rule.
From MaRDI portal
Publication:1401929
DOI10.1016/S0890-5401(03)00016-6zbMath1054.68143MaRDI QIDQ1401929
Publication date: 19 August 2003
Published in: Information and Computation (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Representing and building models for decidable subclasses of equational clausal logic
- Explicit representation of terms defined by counter examples
- Equational problems and disunification
- 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
- A calculus combining resolution and enumeration for building finite models
- Hyperresolution for guarded formulae
- Using resolution for testing modal satisfiability and building models
- Resolution Strategies as Decision Procedures
- Pruning the search space and extracting more models in tableaux
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Decision procedures and model building in equational clause logic
- Using resolution for deciding solvable classes and building finite models
- An improved lower bound for the elementary theories of trees
- Hyperresolution and automated model building
- A Machine-Oriented Logic Based on the Resolution Principle
- Automatic Theorem Proving With Renamable and Semantic Resolution
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
This page was built for publication: Extracting models from clause sets saturated under semantic refinements of the resolution rule.
