lionell/math-logic
Implementation of sequential method for classic first-order-logic
181
lionell/math-logic repository overview
Sequential method
A prover of logical formulas. Core of application is Sequential Method algorithm.
How it works
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.
Algorithm
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.
Sequential formulas
| 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.
Let's look at examples
Example 1
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.
Example 2
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.
Example 3
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]
Left branch
| 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
Right branch
| 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
Summary
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.
Language specification
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.
Valid expressions
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]
API
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.
API Usage
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.
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 |
Installation
Requirements
- Java Runtime Environment with Java SE8 support
- Maven 3 to build
Building
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.
Running
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
Docker
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.
Used materials
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
Contributions
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.
Licence
MIT
Tag summary
Content type
Image
Digest
Size
474.4 MB
Last updated
over 7 years ago
docker pull lionell/math-logic