Deciding the guarded fragments by resolution

DOI10.1016/S0747-7171(02)00092-5zbMath1012.03046OpenAlexW2076676228MaRDI QIDQ1867216

Hans de Nivelle, Maarten de Rijke

Publication date: 2 April 2003

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0747-7171(02)00092-5

zbMATH Keywords

modal logicguarded fragmentresolution-based decision procedures

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items

On the complexity of division and set joins in the relational algebra ⋮ Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Hyperresolution for guarded formulae ⋮ Resolution with order and selection for hybrid logics ⋮ A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). ⋮ Deciding regular grammar logics with converse through first-order logic

Uses Software

• OTTER
• SPASS
• Bliksem
• FLOTTER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Definability with bounded number of bound variables
• Modal resolution in clausal form
• Modal languages and bounded fragments of predicate logic
• Resolution methods for the decision problem
• Expressiveness of concept expressions in first-order description logics
• A note on assumptions about Skolem functions
• On languages with two variables
• The Computational Complexity of Provability in Systems of Modal Propositional Logic
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• On the Decision Problem for Two-Variable First-Order Logic
• Decision-algorithms for the associativity of latin squares