A research project in path semantics, a re-interpretation of functions for expressing mathematics

a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features

Keith Devlin's Introduction to Mathematical Thinking course on Coursera (2017 Spring)

UCalgary version of forallx, an introduction to formal logic

The Slate Interactive Theorem Prover

The lecture notes for my discrete mathematics classes.

Python library for computational formal logic, formal semantics, and theorem proving

An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.

An interpreter for Gödel's System T

A self-taught project about Machine Learning & Deep Learning with Python. Thanks to the countless researchers and developers around the world and their open-source code, particularly Python-based open-source code!

Human Logic

This repository is designed to provide all the necessary resources for the second year preparatory cycle at ENSIA.

Python package that provides an interface to work with classical propositional and first-order logic, based on my solutions to the textbook Mathematical Logic Through Python by Nisan and Gonczarowski

veblen function in agda

Automated mathematical theorem formulation deduced from a provided set of axioms. Builds upon the HRL theorem generator.

A proof-of-concept LCF-style interactive theorem prover for HOL(C)

HLM mathematical library for the Slate interactive theorem prover

Generate Stack Math puzzles with this handy utility written in Visual Basic

Implementation of Russel paradox in Idris 2

first-order logic and set theory