Automatic proofs and counterexamples for some ortholattice identities

DOI10.1016/S0020-0190(98)00015-5MaRDI QIDQ293265zbMATH OpenOpenAlexWikidataFDO

Authors William McCune

Publication date 9 June 2016

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL http://www.sciencedirect.com/science/article/pii/S0020019098000155?np=y

zbMATH Keywords

automatic theorem provingortholatticequantum logic

Mathematics Subject Classification ID

Quantum logic (03G12) Complemented lattices, orthocomplemented lattices and posets (06C15)

Recommendations

• Combinatorial and automated proofs of certain identities
• Automated proofs for some Stirling number identities
• Automated proofs of the Moufang identities in alternative rings
• scientific article; zbMATH DE number 3938594
• scientific article; zbMATH DE number 434742
• Automatic proofs for formulae enumerating proper polycubes
• Automatic proofs for formulae enumerating proper polycubes
• Generalized identities with automorphisms
• scientific article; zbMATH DE number 3014016
• Proof and generalization of the Cassini-Catalan-Tagiuri-Gould identities

Cites work

• Automated deduction in equational logic and cubic curves
• scientific article; zbMATH DE number 1283787 (Why is no real title available?)
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• Orthomodularity is not elementary

Cited in

(5)

• Automated discovery of single axioms for ortholattices
• Automatic proofs for formulae enumerating proper polycubes
• Implementing the binding and accommodation theory for anaphora resolution and presupposition projection
• scientific article; zbMATH DE number 4072440 (Why is no real title available?)
• Decidability in orthomodular lattices

Describes a project that uses

Uses Software

• OTTER
• Mace4
• EQP

This page was built for publication: Automatic proofs and counterexamples for some ortholattice identities

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