Automatic proofs and counterexamples for some ortholattice identities

DOI10.1016/S0020-0190(98)00015-5zbMATH Open1338.03114OpenAlexW1984341203WikidataQ124814624 ScholiaQ124814624MaRDI QIDQ293265FDOQ293265

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

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

zbMATH Keywords

quantum logicautomatic theorem provingortholattice

Mathematics Subject Classification ID

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

Cites Work

• Automated deduction in equational logic and cubic curves
• Orthomodularity is not elementary
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (5)

• Title not available (Why is that?)
• Decidability in orthomodular lattices
• Automatic proofs for formulae enumerating proper polycubes
• Automated discovery of single axioms for ortholattices
• Implementing the Binding and Accommodation Theory for Anaphora Resolution and Presupposition Projection

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)