# propositional-tableau-solver-rs 0.1.0

Propositional tableau solver for propositional formulas
Documentation

# Propositional Tableaux Solver

A little propositional formula satisfiability solver using the propositional tableaux method, written in the Rust programming language!

## Syntax of Propositional Formula

The input to the solver must be a well-formed propositional formula.

It can be described by the following BNF grammar:

``````<formula>   ::= <propositional-variable>
|   ( - <formula> )             # negation
|   ( <formula> ^ <formula>  )  # conjunction
|   ( <formula> | <formula>  )  # disjunction
|   ( <formula> -> <formula>  ) # implication
|   ( <formula> <-> <formula> ) # bi-implication
``````

Whitespaces are stripped and ignored, and a `<propositional-variable>` can be any sequence of alphanumeric characters `[a-zA-Z][a-zA-Z0-9]*` that begin with a alphabet character. Cases are respected and `aaa` is a different propositional variable from `AAA`.

## Running via Cargo

### Mode

The CLI supports both `satisfiability` mode and `validity` mode checking for a given propositional formula.

Use the `-m` mode switch:

1. Validity mode: `-m v`.
2. Satisfiability mode (default): `-m s`.

### Input

Two ways to supply the propositional formula exist, with the `-c` switch method taking precedence:

1. CLI argument switch `-c <input_string>`
2. IO redirection

#### Command-line String

Using the `-c <input_string>`

``````\$ cargo run -c "(a^b)"
``````

#### IO Redirection

Alternatively, redirect the standard input `stdin` to the solver to supply the propositional formula.

``````\$ cat input.txt > cargo run
``````