Theorem Proving in Higher Order Logics
From MaRDI portal
Publication:5464649
DOI10.1007/b100400zbMath1099.68734OpenAlexW2798038182MaRDI QIDQ5464649
Publication date: 18 August 2005
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b100400
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (13)
Two cryptomorphic formalizations of projective incidence geometry ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method ⋮ Measuring the readability of geometric proofs: the area method case ⋮ Towards an intelligent and dynamic geometry book ⋮ The area method. A recapitulation ⋮ A review and prospect of readable machine proofs for geometry theorems ⋮ A case study in formalizing projective geometry in Coq: Desargues theorem ⋮ A graphical user interface for formal proofs in geometry ⋮ A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs ⋮ Automatic Verification of Regular Constructions in Dynamic Geometry Systems ⋮ Formalization of Wu’s Simple Method in Coq ⋮ GeoThms — a Web System for Euclidean Constructive Geometry
Uses Software
This page was built for publication: Theorem Proving in Higher Order Logics
