scientific article; zbMATH DE number 440110

MaRDI QIDQ3142019zbMATH OpenFDO

Authors Alexander Leitsch

Publication date 14 June 1994

zbMATH Keywords

Herbrand interpretationHorn clausesKrom clausessemantic clash resolution

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Logic programming (68N17)

Recommendations

• scientific article; zbMATH DE number 512974
• scientific article; zbMATH DE number 19146
• scientific article; zbMATH DE number 7680806
• Extracting models from clause sets saturated under semantic refinements of the resolution rule.
• Resolution decision procedures

Cited in

(12)

• Extracting models from clause sets saturated under semantic refinements of the resolution rule.
• Hyperresolution for guarded formulae
• scientific article; zbMATH DE number 4053070 (Why is no real title available?)
• Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
• scientific article; zbMATH DE number 2090304 (Why is no real title available?)
• A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract)
• Decision procedures using model building techniques
• Recognizing unnecessary clauses in resolution based systems
• Representing and building models for decidable subclasses of equational clausal logic
• Some techniques for proving termination of the hyperresolution calculus
• Deciding expressive description logics in the framework of resolution
• 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 Q3142019)