The area method. A recapitulation
type: Item
instance of: scholarly article
title: The area method. A recapitulation
zbMATH Open document ID: 1242.68281
author: Predrag Janičić
author: Julien Narboux
author: Pedro Quaresma
published in: Journal of Automated Reasoning
publication date: 2012-07-17T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 6057743
zbMATH Keywords: area method
zbMATH Keywords: geometry
zbMATH Keywords: automated theorem proving
zbMATH Keywords: formalisation
describes a project that uses: GCLCprover
describes a project that uses: GeoThms
describes a project that uses: Theorema
describes a project that uses: gcl
describes a project that uses: GEX
describes a project that uses: Flyspeck
describes a project that uses: Coq
describes a project that uses: GCLC
describes a project that uses: GeoProof
MaRDI profile type: Publication
full work available at URL: s10817-010-9209-7
OpenAlex ID: W86824626
Wikidata QID: Q57552308
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: \textit{Theorema}: Towards computer-aided mathematical theory exploration
cites work: Q3994509
cites work: Automated reasoning in geometry
cites work: Automated production of traditional proofs in solid geometry
cites work: Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
cites work: Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles
cites work: A deductive database approach to automated geometry theorem proving and discovering
cites work: Automated reasoning in geometry theorem proving with Prolog
cites work: Q4531863
cites work: Automated Deduction in Geometry
cites work: Q3234138
cites work: GCLC — A Tool for Constructive Euclidean Geometry and More Than That
cites work: Automatic Verification of Regular Constructions in Dynamic Geometry Systems
cites work: Geometry constructions language
cites work: Using Gröbner bases to reason about geometry problems
cites work: Formal certification of a compiler back-end or
cites work: A case study in formalizing projective geometry in Coq: Desargues theorem
cites work: Formalizing Projective Plane Geometry in Coq
cites work: Formalizing Hilbert’s Grundlagen in Isabelle/Isar
cites work: Theorem Proving in Higher Order Logics
cites work: A graphical user interface for formal proofs in geometry
cites work: Mechanical Theorem Proving in Tarski’s Geometry
cites work: Plane geometry theorem proving using forward chaining
cites work: Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories
cites work: Q5807665
cites work: The axioms of constructive geometry
cites work: Formalization of Hilbert's geometry of incidence and parallelism
cites work: Q4840652
cites work: Q3838777
cites work: Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method
cites work: Visually dynamic presentation of proofs in plane geometry. II: Automated generation of visually dynamic presentations with the full-angle method and the deductive database method
cites work: Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems
DBLP publication ID: journals/jar/JanicicNQ12
DOI: 10.1007/S10817-010-9209-7
description: scientific article; zbMATH DE number 6057743