| Formula | Input format |
|---|---|
| 0 ∈ X | (zeroin X) |
| X ⊆ Y | (sub X Y) |
| Sing(X) | (sing X) |
| Y = Succ(X) | (succ Y X) |
| X < Y | (< X Y) |
(A and B denotes formulae)
| Formula | Input format |
|---|---|
| ¬A | (neg A) |
| A∧B | (and A B) |
| A∨B | (or A B) |
| A→B | (implies A B) |
| ∃X.A | (exists X A) |
| ∀X.A | (forall X A) |
Use syntax similar to syntax for macros in C
#define (my_predicate list_of_arguments) (...)#define (not_sub X Y) (neg (sub X Y))
(and (not_sub U V) (zeroin V))python3 main.py [--rabit] [--spot] [--validity]
Use --rabit for reduction with a simulation using lookahead 10
Requirements: Install Rabit into a parent directory (../RABIT250/Reduce.jar)
Use --spot for complementation using external tool
Requirements: Install Spot
Use --validity to determine validity of the input formula
The final automaton is saved in a.ba and the graph is in graph.pdf
Formulae used for experiments are in benchmark/
Formula: (x∈Y∧x∉Z) ∨ (x∈Z∧x∉Y)
Input syntax:
(or
(and
(and (sub X Z) (neg (sub X Y)))
(sing X)
)
(and
(sub X Y)
(and (neg (sub X Z)) (sing X))
)
)
a.ba:
[0]
X:1|Y:0|Z:1,[0]->[1]
X:1|Y:1|Z:0,[0]->[1]
X:0|Y:?|Z:?,[1]->[1]
X:0|Y:?|Z:?,[0]->[0]
[1]
graph.pdf:
