A new method for the Boolean ring based theorem proving

DOI10.1006/jsco.1994.1011zbMath0860.03014OpenAlexW2053515248MaRDI QIDQ1333173

Han-Tao 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

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Buchberger's algorithm: A constraint-based completion procedure ⋮ Canonical Ground Horn Theories ⋮ On Theorem Proving in Annotated Logics ⋮ Linear strategy for Boolean ring based theorem proving