| Publication | Date of Publication | Type |
|---|
Automated theorem proving for Metamath
| 2024-11-26 | Paper |
Translating SUMO-K to Higher-Order Set Theory
| 2024-05-03 | Paper |
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
| 2023-02-03 | Paper |
Lash 1.0 (system description)
| 2022-12-07 | Paper |
Prolog Technology Reinforcement Learning Prover
Automated Reasoning | 2022-11-09 | Paper |
GRUNGE: a grand unified ATP challenge
| 2020-03-10 | Paper |
AIM loops and the AIM conjecture
Formalized Mathematics | 2020-03-10 | Paper |
A tale of two set theories
| 2020-01-22 | Paper |
Cantor-Bernstein implies Excluded Middle
| 2019-04-19 | Paper |
Internal guidance for Satallax
Automated Reasoning | 2016-09-05 | Paper |
Extracting Higher-Order Goals from the Mizar Mathematical Library
Lecture Notes in Computer Science | 2016-08-30 | Paper |
Reconsidering pairs and functions as sets
Journal of Automated Reasoning | 2016-05-26 | Paper |
Reducing higher-order theorem proving to a sequence of SAT problems
Journal of Automated Reasoning | 2015-06-23 | Paper |
Glivenko and Kuroda for simple type theory
The Journal of Symbolic Logic | 2014-09-30 | Paper |
Encoding functional relations in Scunak
| 2014-01-10 | Paper |
Satallax: An Automatic Higher-Order Prover
Automated Reasoning | 2012-09-05 | Paper |
Analytic tableaux for higher-order logic with choice
Journal of Automated Reasoning | 2012-07-31 | Paper |
Reducing higher-order theorem proving to a sequence of SAT problems
Lecture Notes in Computer Science | 2011-07-29 | Paper |
scientific article; zbMATH DE number 5872255 (Why is no real title available?)
| 2011-03-30 | Paper |
\(M\)-set models
| 2011-03-30 | Paper |
Analytic tableaux for higher-order logic with choice
Automated Reasoning | 2010-09-14 | Paper |
Automated reasoning in higher-order logic. Set comprehension and extensionality in Church's type theory
| 2010-09-01 | Paper |
Analytic Tableaux for Simple Type Theory and its First-Order Fragment
Logical Methods in Computer Science | 2010-07-27 | Paper |
Terminating tableaux for the basic fragment of simple type theory
Lecture Notes in Computer Science | 2009-12-01 | Paper |
Extended First-Order Logic
Lecture Notes in Computer Science | 2009-10-20 | Paper |
Progress in the Development of Automated Theorem Proving for Higher-Order Logic
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
Cut-Simulation and Impredicativity
Logical Methods in Computer Science | 2009-04-29 | Paper |
Combining Type Theory and Untyped Set Theory
Automated Reasoning | 2009-03-12 | Paper |
Cut-Simulation in Impredicative Logics
Automated Reasoning | 2009-03-12 | Paper |
Formal Representation of Mathematics in a Dependently Typed Set Theory
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
Verifying and Invalidating Textbook Proofs Using Scunak
Lecture Notes in Computer Science | 2007-09-05 | Paper |
TPS: A hybrid automatic-interactive system for developing proofs
Journal of Applied Logic | 2007-02-20 | Paper |
Automated Deduction – CADE-20
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2006-07-06 | Paper |
Higher-order semantics and extensionality
Journal of Symbolic Logic | 2005-08-29 | Paper |
scientific article; zbMATH DE number 2090316 (Why is no real title available?)
| 2004-08-12 | Paper |
scientific article; zbMATH DE number 1614693 (Why is no real title available?)
| 2001-07-05 | Paper |
Explosive nonnegative solutions to two point boundary value problems
Nonlinear Analysis: Theory, Methods & Applications | 1996-02-12 | Paper |
A Formal Proof of R(4,5)=25
| N/A | Paper |
