Hyperresolution for guarded formulae
From MaRDI portal
Publication:1404983
DOI10.1016/S0747-7171(03)00034-8zbMath1020.03007MaRDI QIDQ1404983
Ullrich Hustadt, Renate A. Schmidt, Lilia Georgieva
Publication date: 25 August 2003
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Modal logic (including the logic of norms) (03B45) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Related Items (10)
Simulation and Synthesis of Deduction Calculi ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ Some techniques for proving termination of the hyperresolution calculus ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ Individual Reuse in Description Logic Reasoning ⋮ Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \) ⋮ First-Order Resolution Methods for Modal Logics ⋮ A Resolution-based Model Building Algorithm for a Fragment of OCC1N = ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ A new methodology for developing deduction methods
Cites Work
- A structure-preserving clause form translation
- Modal languages and bounded fragments of predicate logic
- Deciding the guarded fragments by resolution
- Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Resolution-based methods for modal logics
- On the Restraining Power of Guards
- Soft typing for ordered resolution
- Hyper tableaux
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Hyperresolution for guarded formulae
