Features

SAT Solving

Checks if the specified propositions are consistent. See Wiki entry for details.

# example input
prop A -> B
prop C & ~B
cmd solve satisfiability
config solver="sat4j"

Output:

Satisfiable
A=False
B=False
C=True

Conversion

Converts to logical forms. See Grammar entry for details.

# example input
prop A -> (B & C)
cmd convert to CNF

Output:

prop (~A | B) & (~A | C)

Translation

Translates between variants. See Grammar entry for details.

# example input
prop A -> (B & C)
cmd translate to reserved word variant

Output:

prop (A implies (B and C))