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
-
Updated
Nov 16, 2021 - TeX
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
An implementation in Haskell of a tableau-style proof system for the implication-free fragment of intuitionistic propositional logic.
Formal specification of a language of grammars and proofs about their ambiguity
Four color theorem, Guthrie, Kempe, Tait and other people and stuff
Collaborative repo for Big Proof Programme at the Isaac Newton Institute, Jun 26 to Aug 4, 2017
First-Order Logic Automated Theorem Prover using Tableaux Method
A propositional logic equivalence and first-order logic ND prover (wrapper).
Type Theory course ; Master's Degree in Computer Science @ UniPD
Theorem proving in Isabelle
Yet Another First-Order Logic Problem Solver
Definitions and proofs written in Python
Supervisionary: a proof-checking system for HOL
A formalisation of Solèr's theorem using the Isabelle proof assistant
Some examples of programs with dependent types from Type Theory course in IFMO University.
Richard Moot's personal homepage
A graphical interactive proof assistant designed for education. My contributions: applying rules by elimination, proofs by induction, proofs by cases, multi-axiom element and misc css styling. Honours report grade: 76% 🎉
🧮 Mathematical theorem proving assistant.
A kernel using inference rules in order to compute the three of proves.
Add a description, image, and links to the theorem-proving topic page so that developers can more easily learn about it.
To associate your repository with the theorem-proving topic, visit your repo's landing page and select "manage topics."