| Publication | Date of Publication | Type |
|---|
Theorem proving as constraint solving for coherent logic with function symbols
Journal of Automated Reasoning | 2025-11-26 | Paper |
| Automated completion of statements and proofs in synthetic geometry: an approach based on constraint solving | 2025-09-03 | Paper |
| Automated generation of illustrations for synthetic geometry proofs | 2024-12-17 | Paper |
Automated generation of illustrated proofs in geometry and beyond
Annals of Mathematics and Artificial Intelligence | 2024-01-08 | Paper |
Theorem proving as constraint solving with coherent logic
Journal of Automated Reasoning | 2022-12-12 | Paper |
New dynamics in dynamic geometry: dragging constructed points
Journal of Symbolic Computation | 2019-11-07 | Paper |
scientific article; zbMATH DE number 7056222 (Why is no real title available?)
(available as arXiv preprint) | 2019-05-17 | Paper |
Portfolio theorem proving and prover runtime prediction for geometry
Annals of Mathematics and Artificial Intelligence | 2019-05-16 | Paper |
| scientific article; zbMATH DE number 6984221 (Why is no real title available?) | 2018-11-23 | Paper |
Constructibility classes for triangle location problems
Mathematics in Computer Science | 2016-06-16 | Paper |
Automated theorem proving in GeoGebra: current achievements
Journal of Automated Reasoning | 2016-05-26 | Paper |
Wernick's list: a final update
Forum Geometricorum | 2016-03-24 | Paper |
Proving correctness of a KRK chess endgame strategy by using Isabelle/HOL and Z3
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Computer theorem proving for verifiable solving of geometric construction problems
Automated Deduction in Geometry | 2015-11-11 | Paper |
Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
Annals of Mathematics and Artificial Intelligence | 2015-07-27 | Paper |
A vernacular for coherent logic
Lecture Notes in Computer Science | 2014-08-07 | Paper |
GeoThms -- a web system for Euclidean constructive geometry
Electronic Notes in Theoretical Computer Science | 2013-12-20 | Paper |
Learning strategies for mechanised building of decision procedures
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
URSA: a system for uniform reduction to SAT
Logical Methods in Computer Science | 2012-10-22 | Paper |
Towards understanding triangle construction problems
Lecture Notes in Computer Science | 2012-09-07 | Paper |
CDCL-Based Abstract State Transition System for Coherent Logic
Lecture Notes in Computer Science | 2012-09-07 | Paper |
The area method. A recapitulation
Journal of Automated Reasoning | 2012-07-17 | Paper |
Formalization of Abstract State Transition Systems for SAT
Logical Methods in Computer Science | 2012-04-02 | Paper |
Real-World Reasoning: Toward Scalable, Uncertain Spatiotemporal, Contextual and Causal Inference
Atlantis Thinking Machines | 2012-03-16 | Paper |
A coherent logic based geometry theorem prover capable of producing formal and readable proofs
Automated Deduction in Geometry | 2011-11-25 | Paper |
GCLC -- a tool for constructive Euclidean geometry and more than that
Lecture Notes in Computer Science | 2010-09-14 | Paper |
URBiVA: uniform reduction to bit-vector arithmetic
Automated Reasoning | 2010-09-14 | Paper |
| scientific article; zbMATH DE number 5713654 (Why is no real title available?) | 2010-05-28 | Paper |
Geometry constructions language
Journal of Automated Reasoning | 2010-01-25 | Paper |
Automatic Verification of Regular Constructions in Dynamic Geometry Systems
Automated Deduction in Geometry | 2008-04-01 | Paper |
Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories
Lecture Notes in Computer Science | 2007-09-05 | Paper |
Simple characterization of functionally complete one-element sets of propositional connectives
MLQ | 2007-02-07 | Paper |
Frontiers of Combining Systems
Lecture Notes in Computer Science | 2006-10-10 | Paper |
| scientific article; zbMATH DE number 2010170 (Why is no real title available?) | 2003-11-26 | Paper |
| scientific article; zbMATH DE number 1929303 (Why is no real title available?) | 2003-06-17 | Paper |
GD-SAT model and crossover line
Journal of Experimental & Theoretical Artificial Intelligence | 2003-03-17 | Paper |
A general setting for flexibly combining and augmenting decision procedures
Journal of Automated Reasoning | 2002-08-20 | Paper |
| scientific article; zbMATH DE number 1341612 (Why is no real title available?) | 1999-09-22 | Paper |
| scientific article; zbMATH DE number 871441 (Why is no real title available?) | 1996-09-22 | Paper |
