Hyperresolution for guarded formulae

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)

zbMATH Keywords

decidabilityguarded fragmentdecision procedurehyperresolutionhypertableauxmodel builder

Mathematics Subject Classification ID

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

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

• 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
• 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