Type inference algorithms and intuitionistic propositional theorem provers solving type inhabitation problems

Autonomous Theorem Prover for First Order Predicate Logic

Haskell Tautology Checker and Parser

Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]

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.

semantic tableau is method of finding whether the given logic (propositional logic here) is consistent or inconsistent, whether it is valid (tautology) or not.

This repository contains my projects created during Language and Libraries of Data Analysis on AGH