The following pages link to (Q3142019):
Displaying 10 items.
- Recognizing unnecessary clauses in resolution based systems (Q688549) (← links)
- 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)
- Extracting models from clause sets saturated under semantic refinements of the resolution rule. (Q1401929) (← links)
- Hyperresolution for guarded formulae (Q1404983) (← links)
- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models (Q4610336) (← links)
- A Resolution-based Model Building Algorithm for a Fragment of OCC1N = (Q4916224) (← links)
- Decision procedures using model building techniques (Q6560165) (← links)
