scientific article; zbMATH DE number 2090304

zbMATH Open1072.68573MaRDI QIDQ4809060FDOQ4809060

Authors: Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt 

Publication date: 12 August 2004

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2392/23920260.htm

Title of this publication is not available (Why is that?)

Recommendations

• Resolution decision procedures
• scientific article; zbMATH DE number 440110
• scientific article; zbMATH DE number 515732
• Hyperresolution and automated model building
• BDI: a new decidable clause class

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (8)

• Extracting models from clause sets saturated under semantic refinements of the resolution rule.
• Simulation and synthesis of deduction calculi
• A new methodology for developing deduction methods
• Representing and building models for decidable subclasses of equational clausal logic
• Some techniques for proving termination of the hyperresolution calculus
• A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
• BDI: a new decidable clause class
• First-order resolution methods for modal logics

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 Q4809060)