Pages that link to "Item:Q1310269"
From MaRDI portal
The following pages link to Resolution methods for the decision problem (Q1310269):
Displaying 32 items.
- Representing and building models for decidable subclasses of equational clausal logic (Q861367) (← links)
- Some techniques for proving termination of the hyperresolution calculus (Q861692) (← links)
- Deciding expressive description logics in the framework of resolution (Q924723) (← links)
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). (Q928657) (← links)
- Decision tactics for derivation search in the resolution method (Q1115412) (← links)
- Extracting models from clause sets saturated under semantic refinements of the resolution rule. (Q1401929) (← links)
- Model building with ordered resolution: Extracting models from saturated clause sets (Q1404975) (← links)
- A calculus combining resolution and enumeration for building finite models (Q1404976) (← links)
- Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators (Q1432885) (← links)
- Deciding the \(E^+\)-class by an a posteriori, liftable order (Q1577484) (← links)
- Deciding the guarded fragments by resolution (Q1867216) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies (Q2456542) (← links)
- An overview of resolution decision procedures (Q2702565) (← links)
- Resolution decision procedures (Q2751377) (← links)
- A Resolution-Based Decision Procedure for $\mathcal{SHOIQ}$ (Q3613440) (← links)
- (Q3770294) (← links)
- Robust solutions and methods in decision-aid (Q4269766) (← links)
- Ordered tableaux: Extensions and applications (Q4610325) (← links)
- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models (Q4610336) (← links)
- A resolution theorem prover for intuitionistic logic (Q4647496) (← links)
- Semantic trees revisited: Some new completeness results (Q4647548) (← links)
- Optimized encodings of fragments of type theory in first order logic (Q4647585) (← links)
- Constructing Bachmair-Ganzinger Models (Q4916082) (← links)
- A Resolution-based Model Building Algorithm for a Fragment of OCC1N = (Q4916224) (← links)
- A method for building models automatically. Experiments with an extension of OTTER (Q5210763) (← links)
- Detecting non-provable goals (Q5210774) (← links)
- Semantic tableaux with ordering restrictions (Q5210807) (← links)
- A classification of non-liftable orders for resolution (Q5234716) (← links)
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models (Q5927982) (← links)
- Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments (Q6149592) (← links)
- Decision procedures using model building techniques (Q6560165) (← links)
