Creusot helps you prove your code is correct in an automated fashion.

CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

This repository contains a collection of papers and resources on Reasoning in Large Language Models.

Synthesis of Heap-Manipulating Programs from Separation Logic

A verification toolchain for Rust programs

Frama-C and WP tutorial

Deductive synthesis and compilation of specialized databases.

From Symbolic Logic Reasoning to Soft Reasoning: A Neural-Symbolic Paradigm

An OpenAI gym environment for automated rule-based deductive program verification in KeY.

Multi-Step Deductive Reasoning Over Natural Language: An Empirical Study on Out-of-Distribution Generalisation

A Diagnostic Benchmark for Evaluating Logical Robustness of Deductive Reasoners

Deductive Commonsense Reasoning

Naive, bottom-up Datalog semantics, in about 200 lines

Okami is a next generation solver for Datalog. It is based on specializating a Datalog's resolution technique to compile a program into a relational algebra abstract machine that is extremely efficient computing solutions for the database

Deduction Rules for Ontology Reasoning