Skip to content

Logical expressions prover using equivalence laws

License

Notifications You must be signed in to change notification settings

Eric-exe/LogiXpr

Repository files navigation

LogiXpr

License Static Badge GitHub repo size

LogiXpr is a C++ console application that evaluates boolean expressions. It supports the following operators:

  • ! - not
  • & - and
  • | - or
  • ^ - xor
  • -> - implies
  • <=> - if and only if

It also supports the following constants:

  • T - true
  • F - false

And variables from a to z.

How it works

LogiXpr utilizes the shunting yard algorithm to convert expressions into abstract syntax trees (ASTs). These ASTs are subsequently evaluated to determine their equivalence using a truth table analysis. If an equivalence is detected, LogiXpr proceeds to recursively evaluate the initial AST by testing each node against the possible equivalences defined in the include\equivLaws.h file.

To find the shortest equivalent expression, LogiXpr employs a breadth-first search algorithm. This search algorithm systematically explores various transformations and evaluates the resulting expressions at each level. By leveraging the breadth-first search approach, LogiXpr efficiently identifies the shortest equivalent expression by considering all possible transformations at each step before delving deeper into the search space.

config.ini

If the application cannot generate a proof:

  • Couldn't find a solution :(: Increase the max expression length in your config file.
  • Too many in queue :(: Increase the max queue size depending on your RAM. Alternatively, if you believe that each expression in the proof is short, it may be better to decrease the max expression length.

Preview

Installation

To build and install LogiXpr, you will need to have CMake installed on your system. You can download CMake from the official website: https://cmake.org/download/.

  1. Clone the repository
git clone https://github.com/ericlin-jpg/LogiXpr.git
  1. Create a build directory
cd LogiXpr
mkdir build
cd build
  1. Run CMake
cmake ..
  1. Build the project
cmake --build . --config Release
  1. Go to the ..\bin\Release directory and run the executable
cd ..\bin\Release
./LogiXpr

Running Unit Tests

To run the unit tests in tests, run build.sh.

About

Logical expressions prover using equivalence laws

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published