Simplifying von Plato's axiomatization of constructive apartness geometry

DOI10.1016/S0168-0072(99)00031-7MaRDI QIDQ1964142zbMATHOpenAlexFDO

Authors Da-Fa Li, Peifa Jia, Xin-Xin Li

Publication date 29 June 2000

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(99)00031-7

zbMATH Keywords

constructive geometryapartness geometryintuitionistic axiom system

Mathematics Subject Classification ID

General theory of linear incidence geometry and projective geometries (51A05) Subsystems of classical logic (including intuitionistic logic) (03B20) Foundations of classical theories (including reverse mathematics) (03B30) Other constructive mathematics (03F65) Intuitionistic mathematics (03F55)

Recommendations

• Using the prover ANDP to simplify orthogonality.
• Simplifying the axiomatization for ordered affine geometry via a theorem prover
• Quantifier-free axioms for constructive affine plane geometry
• The axioms of constructive geometry
• A further simplification of Tarski's axioms of geometry

Cites work

• 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
• 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

(8)

• Complete independence of an axiom system for central translations
• Axiomatizing geometric constructions
• Quantifier-free axioms for constructive affine plane geometry
• Using the prover ANDP to simplify orthogonality.
• Simplifying the axiomatization for ordered affine geometry via a theorem prover
• The axioms of constructive geometry
• `Outside' as a primitive notion in constructive projective geometry
• A common axiom set for classical and intuitionistic plane geometry

This page was built for publication: Simplifying von Plato's axiomatization of constructive apartness geometry

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