Current
-
Profound-Intuitionistic, aka Profint, is an
interactive theorem prover for first-order intuitionistic
logic that is designed around expressive direct manipulation
based interactions. It runs in your browser and produces
proofs for a variety of backend verifiers, including Coq,
Lean, and Isabelle/HOL.
- K. Chaudhuri. Subformula Linking for Intuitionistic Logic with Application to Type Theory. International Confernce on Automated Deduction (CADE). LNCS 12699, pp. 200–216. 2021. ©Springer
- K. Chaudhuri, P. Donato, L. Massacci, and B. Werner. Certifying Proof-By-Linking. INRIA. Technical Report HAL-04317972. 2022.
- The Abella interactive theorem prover, which is
well suited for formalizing the meta-theory of deductive systems.
- You can run Abella in your browser in addition to a separate tool.
- D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur, A. Tiu, and Y. Wang. Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning. Volume 7(2). 2014.
- The Distributed Assertion Management Framework (DAMF)
is a proposal for a heterogeneous network of reasoning agents
to exchange and reuse assertions while cryptographically
tracking provenance and trust.
- There is a DAMF-aware branch of Abella
- F. Al Wardani, K. Chaudhuri, and D. Miller. Formal Reasoning using Distributed Assertions. International Symposium on Frontiers of Combining Systems (FroCoS). LNCS 14279, pp. 176–194. 2023. ©Springer
- The Maetning (dis)prover for first-order
intuitionistic logic, that is well suited to finding a reason
for a non-theorem to be false.
- T. Brock-Nannestad and K. Chaudhuri. Disproving Using the Inverse Method by Iterated Refinement of Finite Approximations. Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-24), Wrocław, Poland. LNCS 9323, pp. 153–168. September 2015. ©Springer. See the associated theorem prover, Mætning.
Older
- The Sympli family of theorem provers for linear logic which I wrote during my PhD. Written in Standard ML. (BSD 2-clause license.)
- The TLA+ Proof System, a suite of tools for reasoning about Leslie Lamport’s Temporal Logic of Actions. I built the Proof Manager component of this system during 2007-2008. Written in OCaml and Java. ©Microsoft and Inria