Using the prover ANDP to simplify orthogonality.

DOI10.1016/S0168-0072(03)00051-4MaRDI QIDQ1412831zbMATH OpenOpenAlexFDO

Authors Da-Fa 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

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

Recommendations

• Simplifying von Plato's axiomatization of constructive apartness geometry
• OTTER proofs in Tarskian geometry
• Simplifying the axiomatization for ordered affine geometry via a theorem prover
• The axioms of constructive geometry
• Finding proofs in Tarskian geometry

Cites work

• scientific article; zbMATH DE number 1324436 (Why is no real title available?)
• Logic and structure
• 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
• Simplifying von Plato's axiomatization of constructive apartness geometry
• Single axioms for the left group and right group calculi
• 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
• Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving

Cited in

(3)

• Simplifying the axiomatization for ordered affine geometry via a theorem prover
• Axiomatizing geometric constructions
• Simplifying von Plato's axiomatization of constructive apartness geometry

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

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