Yet Another Sat solvER

A logical solver based on resolution by refutation. It determines whether a set of clauses, expressed in simplified conjunctive normal form (CNF), is satisfiable or not. In addition to be able to simplify a formula expressed in propositional language into CNF.

A Python library providing basic functionalities for manipulating propositional logic

A propositional logic prover implemented using resolution refutation.

Propositional theorem prover - resolution with pure literal elimination and subsumption elimination, implemented in ISO Prolog. Educational software.

Performs normal form conversions of propositional formulas through the use of syntax trees, and provides 3 sat-solver algorithms with verifiable step-by-step output.

A Propositional Logic Interpreter written in Node.js

In this bachelor thesis, I developed a toolkit for automated reasoning and interpolation with ordered resolution.

resolution refutation is method of finding whether the given antecedent implies the consequent or not, it could also be used to check validity of the expressions.

This repository for implementations of Artificial intelligence algorithms

A simple theorem prover made for a university programming assignment