scientific article; zbMATH DE number 19146

MaRDI QIDQ3976574zbMATH OpenFDO

Authors Christian G. Fermüller

Publication date 26 June 1992

zbMATH Keywords

resolutionHorn clausedecision method

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 512974
• scientific article; zbMATH DE number 4047185
• Solving constrained Horn clauses using dependence-disjoint expansions
• scientific article; zbMATH DE number 3860436
• On generalized Horn formulas and k-resolution
• Combinatorial Problems for Horn Clauses
• Read-once resolutions in Horn formulas

Cited in

(15)

• scientific article; zbMATH DE number 4114095 (Why is no real title available?)
• On renaming a set of clauses as a Horn set
• scientific article; zbMATH DE number 4037814 (Why is no real title available?)
• A formal grammatical model of the resolution method for the propositional calculus
• Deciding \(\mathcal H_1\) by resolution
• Some techniques for proving termination of the hyperresolution calculus
• scientific article; zbMATH DE number 516992 (Why is no real title available?)
• scientific article; zbMATH DE number 437521 (Why is no real title available?)
• scientific article; zbMATH DE number 3978440 (Why is no real title available?)
• scientific article; zbMATH DE number 1418449 (Why is no real title available?)
• A linear algorithm for renaming a set of clauses as a Horn set
• An overview of resolution decision procedures
• Combinatorial Problems for Horn Clauses
• scientific article; zbMATH DE number 440110 (Why is no real title available?)
• scientific article; zbMATH DE number 1555187 (Why is no real title available?)

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