Resolution Strategies as Decision Procedures
From MaRDI portal
Cited in
(35)- A method for simultaneous search for refutations and models by equational constraint solving
- Extracting models from clause sets saturated under semantic refinements of the resolution rule.
- Loop checking in SLD-derivations by well-quasi-ordering of goals
- Deciding the E^+-class by an a posteriori, liftable order
- Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic
- Structured proof procedures
- SGGS decision procedures
- Set of support, demodulation, paramodulation: a historical perspective
- Logical reduction of metarules
- Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
- Unsorted functional translations
- History and prospects for first-order automated deduction
- A theory of data dependencies over relational expressions
- Automatic theorem proving. II
- SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
- Using resolution for deciding solvable classes and building finite models
- Semantic trees revisited: some new completeness results
- The blossom of finite semantic trees
- A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
- Proof normalization for resolution and paramodulation
- Semantic tableaux with ordering restrictions
- A classification of non-liftable orders for resolution
- An algorithm for the retrieval of unifiers from discrimination trees
- Rewriting Conjunctive Queries over Description Logic Knowledge Bases
- Maslov's inverse method and decidable classes
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Decision procedures using model building techniques
- Removing redundancy from a clause
- First-order automatic literal model generation
- The complexity of the satisfiability problem for Krom formulas
- Representing and building models for decidable subclasses of equational clausal logic
- Some techniques for proving termination of the hyperresolution calculus
- Deciding expressive description logics in the framework of resolution
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
- Tractable query answering and rewriting under description logic constraints
This page was built for publication: Resolution Strategies as Decision Procedures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4102765)
