Related papers: The Sequent Calculus Trainer - Helping Students to…
The sequent calculus is a formalism for proving validity of statements formulated in First-Order Logic. It is routinely used in computer science modules on mathematical logic. Formal proofs in the sequent calculus are finite trees obtained…
We have developed a web-based pedagogical proof assistant, the Proof Tree Builder, that lets you apply rules upwards from the initial goal in sequent calculus and Hoare logic for a simple imperative language. We equipped our tool with a…
Teaching precise mathematical reasoning can be very hard. It is very easy for a student to make a subtle mistake in a proof which invalidates it, but it is often hard for the teacher to pinpoint and explain the problem in the (often…
Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over several years of teaching a freshman-level course, "Logic and…
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…
Proof assistants and programming languages based on type theories usually come in two flavours: one is based on the standard natural deduction presentation of type theory and involves eliminators, while the other provides a syntax in…
MiniCalc is a web app for teaching first-order logic based on a minimal sequent calculus. As an option the proofs can be verified in the Isabelle proof assistant. We present the lessons learned using the tool in recent years at our…
We describe SeCaV, a sequent calculus verifier for first-order logic in Isabelle/HOL, and the SeCaV Unshortener, an online tool that expands succinct derivations into the full SeCaV syntax. We leverage the power of Isabelle/HOL as a proof…
Chase algorithms are indispensable in the domain of knowledge base querying, which enable the extraction of implicit knowledge from a given database via applications of rules from a given ontology. Such algorithms have proved beneficial in…
Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles…
We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem…
While proof is a central component of postsecondary mathematical study, proof construction has historically posed significant difficulties for students who intend to earn mathematics degrees at the undergraduate level. This work is…
The study of propositional logic -- fundamental to the theory of computing -- is a cornerstone of the undergraduate computer science curriculum. Learning to solve logical proofs requires repeated guided practice, but undergraduate students…
The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The {\lambda}{\mu}{\mu}-calculus is a term assignment system for the sequent calculus and a great foundation for compiler…
In parallel to the ever-growing usage of mechanized proofs in diverse areas of mathematics and computer science, proof assistants are used more and more for education. This paper surveys previous work related to the use of proof assistants…
Undergraduate students of artificial intelligence often struggle with representing knowledge as logical sentences. This is a skill that seems to require extensive practice to obtain, suggesting a teaching strategy that involves the…
Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe…
We present Tactician, a tactic learner and prover for the Coq Proof Assistant. Tactician helps users make tactical proof decisions while they retain control over the general proof strategy. To this end, Tactician learns from previously…
The key to the proof-theoretic study of a logic is a proof calculus with a subformula property. Many different proof formalisms have been introduced (e.g. sequent, nested sequent, labelled sequent formalisms) in order to provide such…
Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a…