scientific article; zbMATH DE number 19146
From MaRDI portal
Publication:3976574
[For the entire collection see Zbl 0734.00012.] The author uses resolution strategies as a decision method and shows the decidability of some classes of Horn clause sets fulfilling certain characterizations, e.g., of variable appearance.
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)- Deciding H₁ by resolution
- On renaming a set of clauses as a Horn set
- A linear algorithm for renaming a set of clauses as a Horn set
- A formal grammatical model of the resolution method for the propositional calculus
- An overview of resolution decision procedures
- scientific article; zbMATH DE number 437521 (Why is no real title available?)
- scientific article; zbMATH DE number 440110 (Why is no real title available?)
- Combinatorial Problems for Horn Clauses
- scientific article; zbMATH DE number 3978440 (Why is no real title available?)
- scientific article; zbMATH DE number 4037814 (Why is no real title available?)
- scientific article; zbMATH DE number 516992 (Why is no real title available?)
- A Horn clause that implies an undecidable set of Horn clauses
- scientific article; zbMATH DE number 4114095 (Why is no real title available?)
- scientific article; zbMATH DE number 1418449 (Why is no real title available?)
- Some techniques for proving termination of the hyperresolution calculus
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)
