Logical Consequence Solver (CDCL)

This project is an implementation of the Logical Consequence problem in Propositional Logic using a CDCL (Conflict-Driven Clause Learning) based SAT solver.

It was developed as part of a Mathematical Logic project.

Prerequisites

To build and run this project, you need:

• Java 21

Check your Java version with:

java --version

Installation

Clone the repository:

git clone https://github.com/savecitoo/MathematicalLogicProject.git
cd MathematicalLogicProject

If you don't have git you can download the zip of the file and extract it.

Build

macOS/Linux

./gradlew build

Windows

gradlew build

Run

To make your project run you have to use the following command:

java -jar build/libs/MathematicalLogic-1.0.0.jar

Once the program is running, you can place one or more .txt files inside the input/ directory. When prompted, type the name of a file (without the .txt extension).

The program will:

• interpret the first n − 1 formulas in the file as the theory
• interpret the last formula as the logical consequence to be checked

If you want to stop the program press CTRL+D in Linux/macOS or CTRL+Z in Windows.