Related papers: Natural Deduction Assistant (NaDeA)
The paper is devoted to the introduction of natural deduction systems for some weak subintuitionistic logics, along with proofs of normalization theorems for these systems.
Intelligent tutoring systems have long enabled automated immediate feedback on student work when it is presented in a tightly structured format and when problems are very constrained, but reliably assessing free-form mathematical reasoning…
Representation determines how we can reason about a specific problem. Sometimes one representation helps us find a proof more easily than others. Most current automated reasoning tools focus on reasoning within one representation. There is,…
When should we defer to AI outputs over human expert judgment? Drawing on recent work in social epistemology, I motivate the idea that some AI systems qualify as Artificial Epistemic Authorities (AEAs) due to their demonstrated reliability…
Tackling Natural Language Inference with a logic-based method is becoming less and less common. While this might have been counterintuitive several decades ago, nowadays it seems pretty obvious. The main reasons for such a conception are…
We introduce real induction, a proof technique analogous to mathematical induction but applicable to statements indexed by an interval on the real line. More generally we give an inductive principle applicable in any Dedekind complete…
The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the danger of accumulating errors across theories. Although,…
OnlineProver is an interactive proof assistant tailored for the educational setting. Its main features include a user-friendly interface for editing and checking proofs. The user interface provides feedback directly within the derivation,…
We extend to natural deduction the approach of Linear Nested Sequents and of 2-sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction -- only one…
Using nonstandard analysis (NSA), the proof of the Laplace's formula is given. The usage of NSA reduces the intricacy of taking limit, and the crude line of the proof would be clearly seen, compared to the done with the rigorous classical…
Interactive proof assistants make it possible for ordinary mathematicians to write definitions and theorems in a formal proof language, like a programming language, so that a computer can parse them and check them against the rules of a…
Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However, this only validates truth of a formal claim, which may…
Real-life conjectures do not come with instructions saying whether they they should be proven or, instead, refuted. Yet, as we now know, in either case the final argument produced had better be not just convincing but actually verifiable in…
This work presents the system ANITA (Analytic Tableau Proof Assistant) developed for teaching analytic tableaux to computer science students. The tool is written in Python and can be used as a desktop application, or in a web platform. This…
Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this position paper we first report our proof strategy language based on a meta-tool approach.…
How difficult are interactive theorem provers to use? We respond by reviewing the formalization of Hilbert's tenth problem in Isabelle/HOL carried out by an undergraduate research group at Jacobs University Bremen. We argue that, as…
In settings from fact-checking to question answering, we frequently want to know whether a collection of evidence (premises) entails a hypothesis. Existing methods primarily focus on the end-to-end discriminative version of this task, but…
We formalise the pi-calculus using the nominal datatype package, based on ideas from the nominal logic by Pitts et al., and demonstrate an implementation in Isabelle/HOL. The purpose is to derive powerful induction rules for the semantics…
Agda is a dependently-typed functional programming language, based on an extension of intuitionistic Martin-L\"of type theory. We implement first order natural deduction in Agda. We use Agda's type checker to verify the correctness of…
These are notes on discrete mathematics for computer scientists. The presentation is somewhat unconventional. Indeed I begin with a discussion of the basic rules of mathematical reasoning and of the notion of proof formalized in a natural…