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