scientific article; zbMATH DE number 1341614

MaRDI QIDQ4263163zbMATH OpenFDO

Authors Ullrich Hustadt, Renate A. Schmidt

Publication date 17 February 2000

zbMATH Keywords

Maslov's class Kresolution refinementsolvable classesunsolvable classes

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• Maslov's inverse method and decidable classes
• scientific article; zbMATH DE number 512974
• Resolution decision procedures

Cited in

(11)

• scientific article; zbMATH DE number 4043809 (Why is no real title available?)
• scientific article; zbMATH DE number 4113559 (Why is no real title available?)
• First-order resolution methods for modal logics
• A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
• Maslov's inverse method and decidable classes
• Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
• A uniform one-dimensional fragment with alternation of quantifiers
• On the complexity of Maslov's class K
• Alternating quantifiers in uniform one-dimensional fragments with an excursion into three-variable logic
• Representing and building models for decidable subclasses of equational clausal logic
• A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).

This page was built for publication:

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