Logical Proposition Solver

A command line tool that automatically generates truth tables for user given logical propositions.

🚀 Features

• Dynamic Variables: Automatically identifies and parses user defined variables.
• Fast Evaluation: Uses deduplicated abstract symbol trees as well as memoization caching to increase computational efficiency.
• Step-by-Step: Produces an entire truth table including all intermediary evaluation steps.
• Comparing Propositions: Simply set two propositions equal to one another (=) to determine if they are equivalent.

🛠 Compilation

Prerequisites

• C++ Compiler (GCC, Clang, etc)
• CMake (Version 3.16+)

Building from Source

1. Clone the repository

git clone https://github.com/archerpergande/propsolver.git

2. Create Build Directory

mkdir build
cd build

3. Generate build files

cmake ..

4. Compile Project

cmake --build .

5. Run executable

./propsolver

📖 Usage

Command Line

Useful for one-off evaluations.

./propsolver "~(p v q) -> r" "~(p v q) = ~p ^ ~q"
|------------------------------------------------------|
| p | q | r | (p v q) | (~(p v q)) | ((~(p v q)) -> r) |
|------------------------------------------------------|
| 1 | 1 | 1 |    1    |      0     |         1         |
| 1 | 1 | 0 |    1    |      0     |         1         |
| 1 | 0 | 1 |    1    |      0     |         1         |
| 1 | 0 | 0 |    1    |      0     |         1         |
| 0 | 1 | 1 |    1    |      0     |         1         |
| 0 | 1 | 0 |    1    |      0     |         1         |
| 0 | 0 | 1 |    0    |      1     |         1         |
| 0 | 0 | 0 |    0    |      1     |         0         |
|------------------------------------------------------|

|-------------------------------------------------------------------------------------------|
| p | q | (p v q) | (~(p v q)) | (~p) | (~q) | ((~p) ^ (~q)) | ((~(p v q)) = ((~p) ^ (~q))) |
|-------------------------------------------------------------------------------------------|
| 1 | 1 |    1    |      0     |   0  |   0  |       0       |               1              |
| 1 | 0 |    1    |      0     |   0  |   1  |       0       |               1              |
| 0 | 1 |    1    |      0     |   1  |   0  |       0       |               1              |
| 0 | 0 |    0    |      1     |   1  |   1  |       1       |               1              |
|-------------------------------------------------------------------------------------------|

Runtime

Useful for generate multiple evaluations.

./propsolver
|============================|
| Propositional Logic Solver |
|============================|

Enter an expression (or nothing to quit): ~(p v q) -> r
|------------------------------------------------------|
| p | q | r | (p v q) | (~(p v q)) | ((~(p v q)) -> r) |
|------------------------------------------------------|
| 1 | 1 | 1 |    1    |      0     |         1         |
| 1 | 1 | 0 |    1    |      0     |         1         |
| 1 | 0 | 1 |    1    |      0     |         1         |
| 1 | 0 | 0 |    1    |      0     |         1         |
| 0 | 1 | 1 |    1    |      0     |         1         |
| 0 | 1 | 0 |    1    |      0     |         1         |
| 0 | 0 | 1 |    0    |      1     |         1         |
| 0 | 0 | 0 |    0    |      1     |         0         |
|------------------------------------------------------|

Enter an expression (or nothing to quit): ~(p v q) = ~p ^ ~q
|-------------------------------------------------------------------------------------------|
| p | q | (p v q) | (~(p v q)) | (~p) | (~q) | ((~p) ^ (~q)) | ((~(p v q)) = ((~p) ^ (~q))) |
|-------------------------------------------------------------------------------------------|
| 1 | 1 |    1    |      0     |   0  |   0  |       0       |               1              |
| 1 | 0 |    1    |      0     |   0  |   1  |       0       |               1              |
| 0 | 1 |    1    |      0     |   1  |   0  |       0       |               1              |
| 0 | 0 |    0    |      1     |   1  |   1  |       1       |               1              |
|-------------------------------------------------------------------------------------------|

Operators

Supports all propositional operators.

Operator	Support Symbols	Example
NOT	~, not	~p
AND	&, &&, ^, and	p ^ q
XOR	@, xor	p @ q
OR	|, ||, v, or	p || q
IMPLICATION	->, =>, implies	p -> q
BICONDITIONAL	<->, <=>, =, iff	p <-> q
TRUE	t, true	p && true
FALSE	f, false	p or f
PARENTHESIS	(), []	(p v q) -> r

Variables

• Inline: Single characters are automatically recognized (ex. p, q)
• Multi-word: Phrases enclosed in quotes are treated as a single variable (ex. "It is raining" -> "I will get wet").

🔮 Roadmap

1. Simplify: Ability to simplify large propositions into more condensed versions.
2. User Interaction: Enhance user interface with this program.
3. Performance Benchmarks: Quantify speed of evaluations.
4. Prepositional Logic: Support for predicate calculus (quantifiers).

🤝 Contributing

Contributions are welcome! Please feel free to submit a Pull Request.

📄 License

This project is open source. MIT.