Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments

DOI10.1007/s10817-023-09687-xarXiv2208.05365OpenAlexW4388937114MaRDI QIDQ6149592

Renate A. Schmidt, Sen Zheng

Publication date: 6 February 2024

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2208.05365

zbMATH Keywords

guarded fragmentclique-guarded fragmentloosely guarded fragmentBoolean conjunctive querysaturation-based decision proceduresaturation-based query rewritingunskolemisation

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Bisimulation quantifiers and uniform interpolation for guarded first order logic
• GYO reductions, canonical connections, tree and cyclic schemas, and tree projections
• Modal languages and bounded fragments of predicate logic
• The CADE-14 ATP system competition
• Resolution methods for the decision problem
• Robbers, marshals, and guards: Game theoretic and logical characterizations of hypertree width.
• Conjunctive-query containment and constraint satisfaction
• Loosely guarded fragment of first-order logic has the finite model property
• Interpolation and definability in guarded fragments
• Deciding the guarded fragments by resolution
• The guarded fragment with transitive guards
• Exploiting forwardness: satisfiability and query-entailment in forward guarded fragment
• Combining induction and saturation-based theorem proving
• Induction in saturation-based proof search
• Reasoning in description logics by a reduction to disjunctive datalog
• Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
• Rewriting Guarded Negation Queries
• Taming the Infinite Chase: Query Answering under Expressive Relational Constraints
• System Description: E 1.8
• An Introduction to Description Logic
• Splitting through New Proposition Symbols
• On the Desirability of Acyclic Database Schemes
• Complexity of the Guarded Two-variable Fragment with Counting Quantifiers
• Query evaluation via tree-decompositions
• SCAN—Elimination of predicate quantifiers
• On the Restraining Power of Guards
• Query Rewriting and Optimization for Ontological Databases
• Guarded Ontology-Mediated Queries
• The Triguarded Fragment of First-Order Logic
• Monotone monadic SNP and constraint satisfaction
• The Description Logic Handbook
• Querying the Guarded Fragment with Transitivity
• Querying the Guarded Fragment
• Linking Data to Ontologies
• Guarded Negation
• A comprehensive framework for saturation theorem proving
• Formalizing Bachmair and Ganzinger's ordered resolution prover

This page was built for publication: Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments