Search
Search Results
-
The Naproche-ZF Theorem Prover (Short Paper)
Naproche-ZF is a new experimental open-source natural theorem prover based on set theory; formalizations in Naproche-ZF are written in a controlled...
-
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry
We present an automatic theorem prover for projective incidence geometry. This prover does not consider coordinates. Instead, it follows a...
-
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
We describe the design, implementation and verification of an automated theorem prover for first-order logic with functions. The proof search...
-
Metamorphic Testing of Logic Theorem Prover
The use of Artificial Intelligence methodologies including machine learning for object recognition and other tasks as well as reasoning has recently...
-
Towards a geometry deductive database prover
The Geometry Automated-Theorem-Provers (GATP) based on the deductive database method use a data-based search strategy to improve the efficiency of...
-
Learning Normative Behaviour Through Automated Theorem Proving
Reinforcement learning (RL) is a powerful tool for teaching agents goal-directed behaviour in stochastic environments, and many proposed applications...
-
Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover
The main topic of this article are SGGS decision procedures for fragments of first-order logic without equality. SGGS ( Semantically-Guided...
-
Goéland: A Concurrent Tableau-Based Theorem Prover (System Description)
We describe Goéland, an automated theorem prover for first-order logic that relies on a concurrent search procedure to find tableau proofs, with...
-
Distributed-Prover Interactive Proofs
Interactive proof systems enable a verifier with limited resources to decide an intractable language (or compute a hard function) by communicating...
-
Designing an Inclusive and Accessible Mathematical Learning Environment Based on a Theorem Prover
A novel approach to design an inclusive and accessible mathematical learning environment is presented: The technology of theorem proving shall be...
-
Guiding an Automated Theorem Prover with Neural Rewriting
Automated theorem provers (ATPs) are today used to attack open problems in several areas of mathematics. An ongoing project by Kinyon and Veroff uses...
-
Twee: An Equational Theorem Prover
Twee is an automated theorem prover for equational logic. It implements unfailing Knuth-Bendix completion with ground joinability testing and a...
-
Extending a brainiac prover to lambda-free higher-order logic
Decades of work have gone into develo** efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem...
-
Theorem Proving as Constraint Solving with Coherent Logic
In contrast to common automated theorem proving approaches, in which the search space is a set of some formulae and what is sought is again a (goal)...
-
System Description: A Theorem-Prover for Subregular Systems: The Language Toolkit and Its Interpreter, Plebby
We introduce here a domain-specific language, PLEB. The Piecewise-Local Expression Builder interpreter (plebby) is an interactive system for...
-
A Comprehensive Framework for Saturation Theorem Proving
A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only...
-
Theorem Proving in Dependently-Typed Higher-Order Logic
Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system...
-
Extending a High-Performance Prover to Higher-Order Logic
Most users of proof assistants want more proof automation. Some proof assistants discharge goals by translating them to first-order logic and...
-
A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness
The analytic technique for proving completeness gives a very operational perspective: build a countermodel to the unproved formula from a failed...
-
The Lean 4 Theorem Prover and Programming Language
Lean 4 is a reimplementation of the Lean interactive theorem prover (ITP) in Lean itself. It addresses many shortcomings of the previous versions and...