Publication | Date of Publication | Type |
---|
Automated generation of illustrations for synthetic geometry proofs | 2024-12-17 | Paper |
Automated generation of illustrated proofs in geometry and beyond | 2024-01-08 | Paper |
Theorem proving as constraint solving with coherent logic | 2022-12-12 | Paper |
New dynamics in dynamic geometry: dragging constructed points | 2019-11-07 | Paper |
https://portal.mardi4nfdi.de/entity/Q5376649 | 2019-05-17 | Paper |
Portfolio theorem proving and prover runtime prediction for geometry | 2019-05-16 | Paper |
https://portal.mardi4nfdi.de/entity/Q4556039 | 2018-11-23 | Paper |
Constructibility classes for triangle location problems | 2016-06-16 | Paper |
Automated theorem proving in GeoGebra: current achievements | 2016-05-26 | Paper |
https://portal.mardi4nfdi.de/entity/Q2796478 | 2016-03-24 | Paper |
Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 | 2015-12-02 | Paper |
Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems | 2015-11-11 | Paper |
Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry | 2015-07-27 | Paper |
A Vernacular for Coherent Logic | 2014-08-07 | Paper |
GeoThms — a Web System for Euclidean Constructive Geometry | 2013-12-20 | Paper |
Learning Strategies for Mechanised Building of Decision Procedures | 2013-04-19 | Paper |
URSA: A System for Uniform Reduction to SAT | 2012-10-22 | Paper |
Towards Understanding Triangle Construction Problems | 2012-09-07 | Paper |
CDCL-Based Abstract State Transition System for Coherent Logic | 2012-09-07 | Paper |
The area method. A recapitulation | 2012-07-17 | Paper |
Formalization of Abstract State Transition Systems for SAT | 2012-04-02 | Paper |
Real-World Reasoning: Toward Scalable, Uncertain Spatiotemporal, Contextual and Causal Inference | 2012-03-16 | Paper |
A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs | 2011-11-25 | Paper |
URBiVA: Uniform Reduction to Bit-Vector Arithmetic | 2010-09-14 | Paper |
GCLC — A Tool for Constructive Euclidean Geometry and More Than That | 2010-09-14 | Paper |
https://portal.mardi4nfdi.de/entity/Q3562927 | 2010-05-28 | Paper |
Geometry constructions language | 2010-01-25 | Paper |
Automatic Verification of Regular Constructions in Dynamic Geometry Systems | 2008-04-01 | Paper |
Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic | 2007-11-28 | Paper |
Automated Reasoning | 2007-09-25 | Paper |
Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories | 2007-09-05 | Paper |
Simple characterization of functionally complete one-element sets of propositional connectives | 2007-02-07 | Paper |
Frontiers of Combining Systems | 2006-10-10 | Paper |
https://portal.mardi4nfdi.de/entity/Q4435128 | 2003-11-26 | Paper |
https://portal.mardi4nfdi.de/entity/Q4708424 | 2003-06-17 | Paper |
GD-SAT model and crossover line | 2003-03-17 | Paper |
A general setting for flexibly combining and augmenting decision procedures | 2002-08-20 | Paper |
https://portal.mardi4nfdi.de/entity/Q4263161 | 1999-09-22 | Paper |
https://portal.mardi4nfdi.de/entity/Q4874803 | 1996-09-22 | Paper |