Linear strategy for Boolean ring based theorem proving
From MaRDI portal
Two inference rules are discussed in Boolean ring based theorem proving, and linear strategy is developed. It is shown that both of them are complete for linear strategy. Moreover, by introducing a partial ordering on atoms, pseudo O-linear and O-linear strategies are presented. The former is complete, the latter, however, is complete for clausal theorem proving.
Recommendations
- A new method for the Boolean ring based theorem proving
- Proof strategies in linear logic
- scientific article; zbMATH DE number 1222110
- scientific article; zbMATH DE number 1499088
- Boolean Rings for Intersection-Based Satisfiability
- scientific article; zbMATH DE number 1292302
- On linear rewriting systems for Boolean logic and some applications to proof theory
- Proof theory for linear lattices
- An even closer integration of linear arithmetic into inductive theorem proving
- On structuring proof search for first order linear logic
Cites work
- A new method for the Boolean ring based theorem proving
- Completely non-clausal theorem proving
- Generalized resolution and NC-resolution
- scientific article; zbMATH DE number 3872640 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- On first-order theorem proving using generalized odd-superpositions II
- Refutational theorem proving using term-rewriting systems
Cited in
(3)
This page was built for publication: Linear strategy for Boolean ring based theorem proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1579733)
