Extracting models from clause sets saturated under semantic refinements of the resolution rule.
From MaRDI portal
Publication:1401929
Recommendations
- Model building with ordered resolution: Extracting models from saturated clause sets
- scientific article; zbMATH DE number 515732
- Hyperresolution and automated model building
- Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae
- scientific article; zbMATH DE number 549974
Cites work
- A calculus combining resolution and enumeration for building finite models
- A Machine-Oriented Logic Based on the Resolution Principle
- A method for simultaneous search for refutations and models by equational constraint solving
- An improved lower bound for the elementary theories of trees
- Automatic Theorem Proving With Renamable and Semantic Resolution
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
- Decision procedures and model building in equational clause logic
- Equational problems and disunification
- Explicit representation of terms defined by counter examples
- scientific article; zbMATH DE number 440110 (Why is no real title available?)
- scientific article; zbMATH DE number 46359 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 1341610 (Why is no real title available?)
- scientific article; zbMATH DE number 599028 (Why is no real title available?)
- scientific article; zbMATH DE number 976360 (Why is no real title available?)
- scientific article; zbMATH DE number 1765701 (Why is no real title available?)
- scientific article; zbMATH DE number 2090304 (Why is no real title available?)
- Hyperresolution and automated model building
- Hyperresolution for guarded formulae
- Increasing model building capabilities by constraint solving on terms with integer exponents
- Pruning the search space and extracting more models in tableaux
- Representing and building models for decidable subclasses of equational clausal logic
- Resolution decision procedures
- Resolution methods for the decision problem
- Resolution Strategies as Decision Procedures
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Using resolution for deciding solvable classes and building finite models
- Using resolution for testing modal satisfiability and building models
Cited in
(14)- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Model building with ordered resolution: Extracting models from saturated clause sets
- Layered clause selection for theory reasoning (short paper)
- On the expressivity and applicability of model representation formalisms
- Finding finite Herbrand models
- scientific article; zbMATH DE number 440110 (Why is no real title available?)
- Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae
- scientific article; zbMATH DE number 2090303 (Why is no real title available?)
- Constructing Bachmair-Ganzinger models
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- Logic for Programming, Artificial Intelligence, and Reasoning
- Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- Massive unification
This page was built for publication: Extracting models from clause sets saturated under semantic refinements of the resolution rule.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1401929)
