A new method for the Boolean ring based theorem proving

DOI10.1006/JSCO.1994.1011MaRDI QIDQ1333173zbMATH OpenOpenAlexFDO

Authors Hantao Zhang

Publication date 21 April 1997

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1006/jsco.1994.1011

zbMATH Keywords

completenessreductionsemantic trees\(N\)-strategyBoolean ring approachfirst-order theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Well-behaved inference rules for first-order theorem proving
• Linear strategy for Boolean ring based theorem proving
• scientific article; zbMATH DE number 3930371
• scientific article; zbMATH DE number 782043

Cited in

(7)

• Buchberger's algorithm: a constraint-based completion procedure
• Linear strategy for Boolean ring based theorem proving
• A theorem prover for Boolean BI
• Case studies of Z-module reasoning: Proving benchmark theorems from ring theory
• Canonical ground Horn theories
• Boolean Rings for Intersection-Based Satisfiability
• On Theorem Proving in Annotated Logics

This page was built for publication: A new method for the Boolean ring based theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1333173)