A prover of logical formulas. Core of application is Sequential Method algorithm.
Application is divided in several independent modules:
- Parser parse input string into AST.
- Tokenizer split input expression into lexemes.
- Infix-to-Postfix converter converts infix list of lexemes to RPN(Reverse Polish Notation).
- Abstract Syntax Tree generator converts list of tokens(token = lexeme + additional information) to tree.
- Sequential method logic of application.
- Wrapper wrap results of Sequential method to unique data structure for mapping to JSON.
Now let's move to the heart of application.
Here are description of one algorithm iteration.
- If all leaves are closed, finish with positive verdict.
- If all leaves are atomic, finish with negative verdict.
- For each non-atomic, non-closed leaf
- Expand leaf.
- Simplify result leaves.
- Goto step 1
There is situation when algorithm will go to INFINITE LOOP. In this case we can use König's infinity lemma to finish with negative result.
| mark | notation | branches | |
|---|---|---|---|
| +! | +!A, Σ | -A, Σ | |
| -! | -!A, Σ | +A, Σ | |
| +v | +(A v B), Σ | +A, Σ | +B, Σ |
| -v | -(A v B), Σ | -A, -B, Σ | |
| +& | +(A & B), Σ | +A, +B, Σ | |
| -& | -(A & B), Σ | -A, Σ | -B, Σ |
| +-> | +(A -> B), Σ | -A, Σ | +B, Σ |
| --> | -(A -> B), Σ | +A, -B, Σ | |
| +∃ | +∃xA, Σ | +Ax[y], Σ | |
| -∃ | -∃xA, Σ | -Ax[z1], ..., -Ax[zm], Σ, -∃xA | |
| +∀ | +∀xA, Σ | +Ax[z1], ..., +Ax[zm], Σ, +∀xA | |
| -∀ | -∀xA, Σ | -Ax[y], Σ | |
Where
- y denotes new unique name.
- z1, ..., zm denotes names used in current sequence.
- Ax[y] denotes renomination of predicate from x to y.
First example demonstrates how exactly sequences is expanding when implication and disjunction are in charge.
P[x] = P[x] | Q[x]
|
v
-(P[x] -> P[x] | Q[x])
|
v
+P[x], -(P[x] | Q[x])
|
v
-P[x], -Q[x], +P[x]
|
v
X
As you can see sequential tree has only one branch, and it's closed. According to algorithm above, expression is truthful. It's quite simple example, so let's move to something more interesting.
Here is more complicated example with quantifiers. It's also truthful, but now we have two different closed branches.
#xP[x] -> Q[x] = P[x] -> #xQ[x]
|
v
-((#xP[x] -> Q[x]) -> P[x] -> #xQ[x])
|
v
+(#xP[x] -> Q[x]), -(P[x] -> #xQ[x])
/ \
/ \
v v
-#xP[x], -(P[x] -> #xQ[x]) +Q[x], -(P[x] -> #xQ[x])
| |
v v
-P[x], -(P[x] -> #xQ[x]), -#xP[x] +P[x], -#xQ[x], +Q[x]
| |
v v
+P[x], -#xQ[x], -P[x], -#xP[x] -Q[x], +P[x], +Q[x], -#xQ[x]
| |
v v
X X
As you can see all two branches closed at the same time. So expression is truthful and no counter examples exists.
This example show you how to deal with unclosed sequences, and how to get a counter example.
P[x] -> #xQ[x] = #xP[x] -> Q[x]
|
v
-(P[x] -> #xQ[x] -> #xP[x] -> Q[x])
|
v
+(P[x] -> #xQ[x]), -(#xP[x] -> Q[x])
/ \
/ \
v v
-P[x], -(#xP[x] -> Q[x]) +#xQ[x], -(#xP[x] -> Q[x])
| |
v v
+#xP[x], -Q[x], -P[x] +Q[z], -(#xP[x] -> Q[x])
| |
v v
+P[y], -Q[x], -P[x] +#xP[x], -Q[x], +Q[z]
|
v
+P[w], -Q[x], +Q[z]
| name | delta | values |
|---|---|---|
| x -> a, | P[a] := False, | |
| A | y -> b | P[b] := True, |
| Q[a] := False |
Let's try to build interpretation on this counter example. There are many different options, but we can stop on:
x := integer
P[x] := x == 1
Q[x] := x != x // always false
| name | delta | values |
|---|---|---|
| x -> a, | Q[a] := False, | |
| B | z -> b, | Q[b] := True, |
| w -> c | P[c] := True |
In this case we can use next interpretation:
x := integer
P[x] := (x + x) % 2 == 0 // always true
Q[x] := x % 2 == 1
We have got two unclosed branches. Each one produces unique counter example. Each counter example can give us many different interpretations. We have already built some of them. You can manually check these interpretations, to ensure that expression is false. Just evaluate input expression with these interpretations.
Let's stop at this example and move forward to syntax overview.
This is language grammar in Backus-Naur-Form.
<expression> ::= <formula> "=" <formula>
<formula> ::= [ "(" ]
<predicate>
| <logical-operation>
| <quantifier>
[ ")" ]
<predicate> ::= <predicate-name> "[" <variable-arguments> "]"
<predicate-name> ::= <capital-letter> { <letter> }
<predicate-arguments> ::= <variable-name> { "," <variable-name> }
<variable-name> ::= <letter> { <letter> }
<logical-operation> ::= <unary-operation>
| <binary-operation>
<binary-operation> ::= <formula> <binary-operation-keyword> <formula>
<binary-operation-keyword> ::= "&"
| "|"
| "->"
<unary-operation> ::= "!" <formula>
<quantifier> ::= <quantifier-keyword> <predicate-name> <formula>
<quantifier-keyword> ::= "#" Stands for "exists"
| "@" Stands for "for all"
<letter> ::= "a"
| "b"
| ...
| "z"
<capital-letter> ::= "A"
| "B"
| ...
| "Z"If your expression does not fit this grammar then application will rise an
parser exception and inform you with error field of response.
Some valid examples of expressions:
P[x] = Q[x]P[x] = P[x] | Q[x]#xP[x] -> Q[x] = P[x] -> #xQ[x]#x@yP[x, y] = @y#xP[x, y]P[x] -> #xQ[x] = #xP[x] -> Q[x]P[x] | Q[x] | R[x] | T[x] | S[x] = @xP[x]@xP[x] = Q[x]
There are only one service available, named check. To use it your query
should contains field named expr with expression you want to check.
Both get and post methods are supported.
Simple request check?expr=P[x]=P[x]|Q[x] will give you response
listed below.
{
"tree":{
"root":{
"formulas":[
{
"formula":"P[x] -> Q[x]",
"value":false
}
],
"children":[
{
"formulas":[
{
"formula":"P[x]",
"value":true
},
{
"formula":"Q[x]",
"value":false
}
],
"children":[],
"closed":false
}
],
"closed":false
}
},
"verity":false,
"examples":[
{
"name":"E",
"delta":{
"x":"m"
},
"example":{
"P":{
"[m]":true
},
"Q":{
"[m]":false
}
}
}
],
"error":null
}Now let's look closer to response structure.
| name | type | description | |
|---|---|---|---|
| response | tree | {root: node} | sequential tree with root node |
| verity | Boolean | null, if infinite loop | |
| examples | [example] | list of examples | |
| error | string | error message from server | |
| node | formulas | [formula] | list of formulas |
| children | [node] | list of child nodes | |
| closed | boolean | is sequence closed | |
| formula | formula | string | actual formula |
| value | boolean | logical value | |
| example | name | string | name of example |
| delta | {x -> a} | map of new variable names | |
| example | {P[x] -> val} | map of predicates/variables/values |
- Java Runtime Environment with Java SE8 support
- Maven 3 to build
You can build app using Maven with ease. Just type mvn clean package.
This will generate JAR file target/sequential-method-1.0-SNAPSHOT.jar.
If you are using Maven, you can run application without building using
mvn spring-boot:run.
Or if you have pre-built JAR you can run it by typing:
java -jar target/sequential-method-1.0-SNAPSHOT.jar
You can run this application using prebuild docker image like this docker run -it -p 8080:8080 lionell/math-logic.
Alternatively you can use Docker Compose docker-compose up -d. This will start service locally and expose port 8080.
Here is a list of materials used in app:
- D3.js visualizing sequential tree
- HTML5 UP design of main page
- Spring framework
- Maven app architecture
- Docker isolated environment
Here I want to say thanks to my friend Fetiorin who helped me with this app.
He did a great job on the client-side.
MIT