Predicate

Predicate is a simple library for parsing, evaluating and textually representing predicates (boolean functions).

Install

git clone [email protected]:lamg/predicate.git
cd predicate/cmd/reduce && go install

Example

The following table shows some examples of how reduce works. Using standard input and output makes easier typing the boolean operators, since you can use Vim's multibyte input method (ex: C-k OR writes ∨), and then pipe the selected text using the visual mode to the reduce command, or just store the predicates in a file and then use it as standard input to reduce (reduce < file_with_predicates).

Syntax

The syntax is based on EWD1300 which I have formalized in the following grammar:

predicate = term {('≡'|'≢') term}.
term = junction ({'⇒' junction} | {'⇐' junction}).
junction = factor ({'∨' factor} | {'∧' factor}).
factor =	[unaryOp] (identifier | '(' predicate ')').
unaryOp = '¬'.

Reduction rules

The procedure Reduce applies the following rules while reducing the predicate.

¬true ≡ false
¬false ≡ true
A ∨ false ≡ A
A ∧ true ≡ A
A ∨ true ≡ true
A ∧ false ≡ false
A ∨ B ≡ B ∨ A
A ∧ B ≡ B ∧ A
A ≡ true ≡ A
A ≡ false ≡ ¬A
true ⇒ A ≡ A
false ⇒ A ≡ true
A ⇒ true ≡ true
A ⇒ false ≡ ¬A
A ⇐ B ≡ B ⇒ A
A ≢ B ≡ A ≡ ¬B