4 citations · 5 across the 3 of their papers we have counts for
4 papers
Automated Generation of Illustrations for Synthetic Geometry Proofs
Predrag Janičić, Julien Narboux
We report on a new, simple, modular, and flexible approach for automated generation of illustrations for (readable) synthetic geometry proofs. The underlying proofs are generated u…
Proof-checking Euclid
Michael Beeson, Julien Narboux, Freek Wiedijk
We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possible to those of Euclid, in a l…
Herbrand's theorem and non-Euclidean geometry
Michael Beeson, Pierre Boutry, Julien Narboux
We use Herbrand's theorem to give a new proof that Euclid's parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constru…
A Vernacular for Coherent Logic
Sana Stojanovic, Julien Narboux, Marc Bezem +1
We propose a simple, yet expressive proof representation from which proofs for different proof assistants can easily be generated. The representation uses only a few inference rule…