Using the prover ANDP to simplify orthogonality.

DOI10.1016/S0168-0072(03)00051-4zbMath1034.03010OpenAlexW2025219931MaRDI QIDQ1412831

Dafa Li

Publication date: 25 November 2003

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(03)00051-4

zbMATH Keywords

Automated theorem provingIntuitionistic logicConstructive geometry

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to geometry (51-04) General theory of linear incidence geometry and projective geometries (51A05) Other constructive mathematics (03F65) Linear incidence geometric structures with parallelism (51A15) Congruence and orthogonality in metric geometry (51F20)

Related Items (1)

Axiomatizing geometric constructions

Cites Work

• Unnamed Item
• Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving
• Single axioms for the left group and right group calculi
• Questions concerning possible shortest single axioms for the equivalential calculus: An application of automated theorem proving to infinite domains
• Shortest single axioms for the classical equivalential calculus
• Single identities for lattice theory and for weakly associative lattices
• Single identities for ternary Boolean algebras
• Solution of the Robbins problem
• The axioms of constructive geometry
• Simplifying von Plato's axiomatization of constructive apartness geometry
• Logic and structure

This page was built for publication: Using the prover ANDP to simplify orthogonality.