Hyperresolution for guarded formulae

DOI10.1016/S0747-7171(03)00034-8MaRDI QIDQ1404983zbMATH OpenFDO

Authors Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt

Publication date 25 August 2003

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

zbMATH Keywords

decidabilitydecision procedureguarded fragmenthyperresolutionhypertableauxmodel 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)

Recommendations

• scientific article; zbMATH DE number 1696822
• Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
• Resolution decision procedures
• Hyperresolution and automated model building
• Automated Reasoning

Cites work

• scientific article; zbMATH DE number 1614697 (Why is no real title available?)
• scientific article; zbMATH DE number 440110 (Why is no real title available?)
• scientific article; zbMATH DE number 1189096 (Why is no real title available?)
• scientific article; zbMATH DE number 1189104 (Why is no real title available?)
• scientific article; zbMATH DE number 1341606 (Why is no real title available?)
• scientific article; zbMATH DE number 517065 (Why is no real title available?)
• scientific article; zbMATH DE number 1507191 (Why is no real title available?)
• scientific article; zbMATH DE number 1531967 (Why is no real title available?)
• scientific article; zbMATH DE number 834561 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• A structure-preserving clause form translation
• Combining superposition, sorts and splitting
• Computational Space Efficiency and Minimal Model Generation for Guarded Formulae
• Deciding the guarded fragments by resolution
• Hyper tableaux
• Modal languages and bounded fragments of predicate logic
• On the Restraining Power of Guards
• Resolution decision procedures
• Resolution theorem proving
• Resolution-based methods for modal logics
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Soft typing for ordered resolution
• Tableau methods for modal and temporal logics
• Using resolution for testing modal satisfiability and building models

Cited in

(11)

• Blocking and other enhancements for bottom-up model generation methods
• Extracting models from clause sets saturated under semantic refinements of the resolution rule.
• A new methodology for developing deduction methods
• Simulation and synthesis of deduction calculi
• Individual Reuse in Description Logic Reasoning
• Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
• Representing and building models for decidable subclasses of equational clausal logic
• Some techniques for proving termination of the hyperresolution calculus
• scientific article; zbMATH DE number 1405457 (Why is no real title available?)
• A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
• First-order resolution methods for modal logics

This page was built for publication: Hyperresolution for guarded formulae

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