A resolution decision procedure for fluted logic

DOI10.1007/10721959_34MaRDI QIDQ2723441zbMATH OpenFDO

Authors Renate A. Schmidt, Ullrich Hustadt

Publication date 5 July 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10721959_34

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• Decidability of fluted logic with identity
• Resolution decision procedures
• An overview of resolution decision procedures
• The fluted fragment revisited
• Complexity and nicety of fluted logic

Cited in

(8)

• A new methodology for developing deduction methods
• Decidability of fluted logic with identity
• Harald Ganzinger's legacy: contributions to logics and programming
• First-order resolution methods for modal logics
• The fluted fragment revisited
• Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
• The niceness of the ordered fragment of first-order logic
• Deciding expressive description logics in the framework of resolution

This page was built for publication: A resolution decision procedure for fluted logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2723441)