An Interface for Dedukti

Supervisionary: a proof-checking system for HOL

Four color theorem, Guthrie, Kempe, Tait and other people and stuff

Step-by-step proof for equivalence in propositional logic and ND prover for first-order logic.

Type Theory course ; Master's Degree in Computer Science @ UniPD

Coursework for Automated Reasoning 2021/22 at the University of Edinburgh

Training an LLM to generate mathematical proofs with a formal verifier in Python

Formal verification of GT-SMDN framework in Lean 4. 53 theorems formalised, 28 complete proofs. Companion to 'Protecting Critical Infrastructure' book.

Contains the code from the book "Modelling logic games and puzzles in First Order Logic" https://link.springer.com/book/10.1007/978-3-030-62547-4

Some examples of programs with dependent types from Type Theory course in IFMO University.

Formal specification of a language of grammars and proofs about their ambiguity

🎶 Explore Prolog coding with Vibe Prolog, a simple interpreter designed to run queries and demonstrate logic in programming efficiently.

Theorem proving in Isabelle

Formally Verifying Smart Contracts using Theorem Proving

Zero-configuration Rocq/Coq development environment with pinned toolchain versions, VS Code integration, and automated documentation deployment

TSPASS is a fair automated theorem prover for monodic first-order temporal logic with expanding domain semantics and propositional linear-time temporal logic.

solving-satisfaction-problems-with-theorem-provers

Formalization projects for the Foundation of Software course at EPFL

DDL2THF -- A preprocessor for translating problems in Dyadic Deontic Logic into THF problems