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

solving-satisfaction-problems-with-theorem-provers

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

A Lean nightly installer for CSE 505.

quick and dirty theorem prover

Jumla is a Python package for generating Lean 4 formal verification tasks from Python specifications.

🧠 Explore Prolog with sb0, a streamlined environment for developing logic-based applications and enhancing your programming skills.

This repository contains the code, data generation scripts, and documentation for a computational study exploring the relationships between the cuteness level of anime profile pictures, the beard prominence of users, and the probability that a user is actually a medieval fantasy dwarf.

Automated theorem proving, Logic Programming, Optimization examples.

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

A program that verifies proofs in the F0 proof system

LeanDojo-v2 is an end-to-end framework for training, evaluating, and deploying AI-assisted theorem provers for Lean 4.

📐 Natural language explanations of Lean 4 theorems | MathJax 4.0 rendering • Batch processing • Mathematical notation | Formal verification accessibility

An API for interfacing with Coq through Tactician by external agents

"Natural" Natural Deduction: a Theorem Prover for Propositional Logic

Chainer implementation of FormulaNet

🔍A deep dive into Formal Methods in Software Engineering 📜—exploring automata, logic, verification, and specification techniques to ensure software correctness and reliability.

Code and data for paper "Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving"

a constraint-based syntax-guided synthesis (SyGuS) engine

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