Providing a simple format for the programmatic management, parsing and printing of logical problems and proofs.
Compatibility with the TPTP language used by
most high-end full FOL reasoners, as described in the
TPTP technical manual.
Compatibility with JSON-LD,
see the W3C recommendation.
This is a simple example for the basics of the json syntax for predicate logic as presented in the JSON-LD-LOGIC specification. Later examples will show other features of the json syntax like functions, equality, json-ld syntax conversion, lists, arithmetics, unique symbols and such.
For the introductory examples of logic and automated reasoning without the use or focus on the JSON syntax you may want to check the Solve predicate logic top menu.
Here we first have two facts in the json syntax where predicates (names of relations)
are the first element of a list: ["father","john","pete"]
means
john is the father of pete. We then have a grandfather rule using a quantifier "forall"
for three variables (use only strings with the capital first letter for variables),
"&"
meaning "and", "=>"
meaning "implies".
We will ask whether from these
two facts and a rule we can derive that there exists somebody who has john as a grandfather: the
last formula is a negation of this question, using "not"
with the obvious meaning.
The whole list of statements is treated as a conjunction (and) of all statements.
Why the negation and contradiction? This is just a convenient way to simplify
the problem. Suppose we want to prove a & b => a
. This is true
if and only if -(a & b => a)
is false. Now, the last formula
is equivalent to a & b & -a
. Thus
the input facts and rules stay as they are, and we only negate the conclusion to be proved.
To summarize, giving a goal to be proved from axioms (i.e. known facts / rules) as a negated
statement is just a convenient way to organize proof search and there is nothing really
special about it.
Although comments are not allowed in standard json, gkc accepts both line
comments //
and multi-line comments /* .... */
in json.
The order of statements in the list is not really important, although it may cause minor and essentially unpredictable differences in search behaviour. Essentially, gkc creates and tries out its own search strategies, like SQL databases. It does not follow a pre-determined predictable search strategy like PROLOG.
Input file example1.txt:
[
["father","john","pete"],
["father","pete","mark"],
["forall", ["X","Y","Z"], [[["father","X","Y"], "&", ["father","Y","Z"]], "=>", ["grandfather","X","Z"]]],
// negated question: does there exist somebody who has john as a grandfather?
["forall", ["X"], ["not",["grandfather","john","X"]]]
]
The output is a json object with two keys:
result
indicates whether the proof was found,
answers
contains a list of all answers and proofs for these answers.
Here we did not ask to find a concrete person, so we have only
a single answer containing just a proof
key indicating a list with the
numbered steps of the proof found: each step is either a used input fact / rule or a
derived fact / rule.
The formulas in the proof are always just lists of atoms (called clauses) treated as a disjunction (or).
Observe that
["-father","?:X","pete"]
means the same as ["not" ["father","?:X","pete"]]
.
?:
like ?:X
are free variables
implicitly assumed to be quantified by "forall".
["in","frm_N" ]
means that the clause stems from the fact/rule number
N given as input.
["mp", 1, 2]
means that this clause
was derived by modus ponens (i.e. the
resolution rule)
from previous steps 1 and 2. More concretely, the first literals of both were cut off and
the rest were glued together. ["mp", 3, 4, 5]
means that the clause was first
derived from clauses 3 and 4 and then the clause 5 was used for and additional
simplifying resolution step.
The Resolution (logic) wiki page is a good short intro to the general principles of the derivation rules with the course materials of Geoff Sutcliffe being a suitable continuation towards deeper understanding. However, our examples are understandable without in-depth theoretical background.
Try to modify the example by removing the statement ["father","john","pete"],
and
run the gkc prover again. After ca one second gkc will stop and output
{"result": "proof not found"}
Although the task is trivial, gkc does not attempt to be clever and tries out a large number of search strategies: this is why it takes a second to terminate. You can click on Advanced and select Print level value + runs or any later option in the select list to see the whole process: later options will give huge amounts of output.
In case gkc does not understand the syntax of the input file it will give a json-formatted error typically indicating a culprit line and piece of input like this:
{"error": "syntax error, unexpected URI, expecting '.': file example1.txt place 'as' in line 3:
foo bar ("}
or {"error": "json syntax error: lexical error: invalid char in json text.
"}
You may also want to convert the example to some other language by clicking on
the Convert to button: first select an output language from the box after the button before
conversion."<=>"
, disjunction "|"
and "not"
connectives for a slightly more
complicated family example, this time defining the
grandfather predicate as either a paternal or maternal grandfather.
You can use "not"
, "~"
or "-"
for logical negation not: they have the same meaning.
The tilde ~
and minus -
characters can be used as a prefix of a
symbol to denote negation: the last line could be equivalently written as
["forall", ["X"], ["-grandfather","john","X"]]
.
[
["father","john","eve"],
["mother","eve","mark"],
["forall", ["X","Y","Z"], [
[[["father","X","Y"], "&", ["father","Y","Z"]],
"|",
[["father","X","Y"], "&", ["mother","Y","Z"]]],
"<=>",
["grandfather","X","Z"]]
],
["forall", ["X"], ["not",["grandfather","john","X"]]]
]
Like example 1, but we want to find a concrete person as an answer: we use the special
"$ans"
predicate for this. Deriving a clause containing only atoms with the
"$ans"
predicate means that the proof has been found.
[
["father","john","pete"],
["father","pete","mark"],
["forall", ["X","Y","Z"], [[["father","X","Y"], "&", ["father","Y","Z"]], "=>", ["grandfather","X","Z"]]],
["forall", ["X"], [["grandfather","john","X"],"=>",["$ans","X"]]]
]
Notice that gkc output contains a key "answer": [["$ans","mark"]],
indicating the substitution made for X
: mark is the answer we were looking for.
Modify the example and try out the line
["forall", ["X","Y"], [["grandfather","Y","X"],"=>",["$ans","Y","X"]]]
You will get [["$ans","john","mark"]]
in the output.
Strings prefixed by ?:
like "?:X"
are free variables
implicitly assumed to be quantified by forall.
The ["if" ... "then" ....]
construction is a convenient syntax instead
of implication: a list of formulas before "then"
is treated
as a conjunction premiss of the implication and the list after
"then"
as a disjunction consequent of the implication. For example,
["if", "a", "b", "c", "then", "d", "e"]
is translated as
[["a","&","b","&","c"], "=>", ["d","|","e"]]
.
The "<="
connective stands for implication from right to left.
The full list of infix binary connectives follows the TPTP language:
"|"
for disjunction,
"&"
for conjunction,
"<=>"
for equivalence,
"=>"
for implication,
"<="
for reverse implication,
"<~>"
for non-equivalence (XOR),
"~|"
for negated disjunction (NOR),
"~&"
for negated conjunction (NAND),
"@"
for application, used mainly in the higher-order context in TPTP.
[
[["father","John","pete"]],
[["father","pete","mickey"], ["father","pete","mark"]],
["if", ["father","?:X","?:Y"], ["father","?:Y","?:Z"], "then", ["grandfather","?:X","?:Z"]],
[["$ans","?:X"], "<=", ["grandfather","John","?:X"]]
]
"="
and "!="
stand for equality and inequality and can occur
either in the middle of a three-element list (infix form) or as a first element of the
list (prefix form).
[
[["father","john"],"=","pete"],
[["father","pete"],"=","mark"],
[[["=",["father",["father","john"]],"?:X"]],"=>",["$ans","?:X"]]
]
[
["=",["father","john"],"pete"],
["=",["father","mike"],"pete"],
["=",["mother","john"],"eve"],
["=",["mother","mike"],"eve"],
["=",["father","pete"],"mark"],
["=",["mother","eve"],"mary"],
["grandfather",["father",["father","?:0"]],"?:0"],
["grandfather",["father",["mother","?:0"]],"?:0"],
[["grandfather","mark","?:0"],"=>",["$ans","?:0"]]
]
Following the JSON-LD semantics in
RDF
the objects have an explicit or implicit "@id"
key value while
the other key: value pairs are interpreted
as RDF triplets subject, property, value where subject is the
value of the "@id"
key. These
triplets are represented using the $arc
predicate:
there is an arc with the label property from the subject to value.
The first expression in this example is thus converted to
["$arc","pete","father","john"]
.
The "@logic"
key is used for inserting logical formulas into
the json objects. The "@name"
key is used as non-logical
metainformation, indicating a name of the input formula shown in proofs.
The convenience key "@question"
automatically forms
the implication with the "$ans"
predicate with all the free
variables in its value as arguments.
[
{"@id":"pete", "father":"john"},
{"@id":"mark", "father":"pete"},
{"@name":"gfrule",
"@logic": ["if", ["$arc","?:X","father","?:Y"],["$arc","?:Y","father","?:Z"], "then", ["$arc","?:X","grandfather","?:Z"]]
},
{"@question": ["$arc","?:X","grandfather","john"]}
]
$arc
predicate.
"@question"
key is transformed to
[["$arc","?:X","grandfather","john"], "=>", ["$ans","?:X"]]
.
"gfrule"
is used in the proof.
"@logic"
value, transformed to the conjunction of the logical atoms led by the "$arc"
predicate.
[
{"@id":"pete", "father":"john"},
{"@id":"mark", "father":"pete"},
{"@name":"gfrule",
"@logic": ["if", {"@id":"?:X","father":"?:Y"}, {"@id":"?:Y","father":"?:Z"}, "then", {"@id":"?:X","grandfather":"?:Z"}]
},
{"@question": {"@id":"?:X","grandfather":"john"}}
]
"@context"
key to specify,
for example, namespaces, symbol mapping and types.
JSON-LD-LOGIC expands strings in the object/map by the JSON-LD "@context"
expansion rules.
This example demonstrates the use of multiple values in
["mark","michael"]
and the JSON-LD "@context"
"@base"
and "@type"
keys.
[
{ "@context": {
"@base": "http://people.org/",
"@vocab":"http://bar.org/",
"father":"http://foo.org/father"
},
"@id":"pete",
"@type": "male",
"father":"john",
"son": ["mark","michael"],
"@logic": ["forall",["X","Y"],
[[{"@id":"X","son":"Y"}, "&", {"@id":"X","@type":"male"}],
"=>",
{"@id":"Y","father":"X"}]
]
},
["if", {"@id":"?:X","http://foo.org/father":"?:Y"}, {"@id":"?:Y","http://foo.org/father":"?:Z"},
"then", {"@id":"?:X","grandfather":"?:Z"}
],
{"@question": {"@id":"?:X","grandfather":"john"}}
]
"@context"
transform the property names.
The same property names outside the "@context"
scope have to be presented
as absolute values in a long form.
JSON-LD interprets JSON objects/maps as key values as new things with their own id-s and properties.
JSON-LD-LOGIC interprets and converts such values correspondingly.
Nesting can be arbitrarily deep and nested objects/maps may contain the @logic
key at any level.
The current example contains a nested "child"
value indicating that
the person we describe (with no id given) has two children with ages
10 and 2, but nothing more is known about them. We also know the person
has a father `john`. The rules state the son/daughter and mother/father
correspondence, define children with ages between 19 and 6 as schoolchildren
and define both the maternal and paternal grandfather. The question is to
find a schoolchild with "john"
as a grandfather.
Also, notice the use of the arithmetic predicate "$less"
.
The following TPTP prefix form arithmetic predicates and functions on integers and reals are used with the same meaning as defined in the TPTP arithmetic system:
"$is_int", "$is_real"
.
"$less"`, `"$lesseq"`, `"$greater"`, `"$greatereq"
.
"$to_int"`, `"$to_real"
.
"$to_int"`, `"$to_real"
.
`"$sum", "$difference", "$product",
"$quotient", "$quotient_e",
"$remainder_e", "$remainder_t", "$remainder_f",
"$floor", "$ceiling",
"$uminus", "$truncate", "$round"
.
[
{ "@context": {
"@vocab":"http://foo.org/",
"age":"hasage"
},
"father":"john",
"child": [
{"age": 10},
{"age": 2}
],
"@logic": ["and",
["forall",["X","Y"],[{"@id":"X","child":"Y"}, "<=>", ["or",{"@id":"Y","father":"X"},{"@id":"Y","mother":"X"}]]],
["forall",["X","Y"],[{"@id":"Y","child":"X"}, "<=>", ["or",{"@id":"Y","son":"X"},{"@id":"Y","daughter":"X"}]]]
]
},
["if", {"@id":"?:X","http://foo.org/hasage":"?:Y"}, ["$less",6,"?:Y"], ["$less","?:Y",19],
"then", {"@id":"?:X", "@type": "schoolchild"}],
["if", {"@id":"?:X","http://foo.org/father":"?:Y"}, {"@id":"?:Y","http://foo.org/father":"?:Z"},
"then", {"@id":"?:X","grandfather":"?:Z"}],
["if", {"@id":"?:X","http://foo.org/mother":"?:Y"}, {"@id":"?:Y","http://foo.org/father":"?:Z"},
"then", {"@id":"?:X","grandfather":"?:Z"}],
{"@question": [{"@id":"?:X","grandfather":"john"}, "&", {"@id":"?:X","@type":"schoolchild"}]}
]
"_:crtd_..."
is built for each object/map
without an explicit "@id"
key.
"@graph"
key for two objectives:
"@id"
key but contains "@graph"
,
the value of the latter is
simply a list of objects in the scope of the "@context"
of the object.
JSON-LD-LOGIC converts such lists to conjunctions, each element using
the same expansion rules.
"@id"
key,
the conjunction elements are not interpreted as RDF triplets,
but quads with the "@id"
key value as a fourth element:
the "@id"
value indicates which graph the
arc belongs to. JSON-LD-LOGIC converts such lists using the four-argument
"$narc"
predicate (named arc) with the graph "@id"
value as the last argument.
The current example represents data necessary for detecting a grandfather relation in two trivial named graphs and uses a rule merging the named graphs into one unnamed graph.
[
{
"@id":"bobknows",
"@graph": [
{"@id":"pete", "father":"john"}
]
},
{
"@id":"eveknows",
"@graph": [
{"@id":"mark", "father":"pete"}
]
},
{
"@name":"mergegraphs",
"@logic": [["$narc","?:X","?:Y","?:Z","?:U"],"=>",["$arc","?:X","?:Y","?:Z"]]
},
{
"@name":"gfrule",
"@logic": ["if", {"@id":"?:X","father":"?:Y"}, {"@id":"?:Y","father":"?:Z"}, "then", {"@id":"?:X","grandfather":"?:Z"}]
},
{"@question": {"@id":"?:X","grandfather":"john"}}
]
The RDF semantics of the JSON-LD list value construction using the "@list"
key
like in "clients": {"@list":["a","b","c"]}
requires the construction of a number of
triplets with rdf:first, rdf:rest and rdf:nil
properties.
JSON-LD-LOGIC deviates from this semantics since it can use function terms instead of
triplets.
A list is converted using the special "$list"
function appending a first argument to
the second argument and the "$nil"
constant for an empty list. JSON-LD-LOGIC
defines a predicate and two functions on lists: "$is_list", "$first", "$rest"
The current example defines functions for counting the length of the list and summing
the numeric elements. Then it uses these functions in a rule for deriving a "goodcompany"
type
as an object with at least three customers and revenues over 100. Finally we ask to find an
object with the "goodcompany"
type.
[
{
"@id":"company1",
"clients": {"@list":["a","b","c"]},
"revenues": {"@list":[10,20,50,60]}
},
[["listcount","$nil"],"=",0],
[["listcount",["$list","?:X","?:Y"]],"=",["+",1,["listcount","?:Y"]]],
[["listsum","$nil"],"=",0],
[["listsum",["$list","?:X","?:Y"]],"=",["+","?:X",["listsum","?:Y"]]],
["if",
{"@id":"?:X","clients":"?:C","revenues":"?:R"},
["$greater",["listcount","?:C"],2],
["$greater",["listsum","?:R"],100],
"then",
{"@id":"?:X","@type":"goodcompany"}
],
{"@question": {"@id":"?:X","@type":"goodcompany"}}
]
JSON-LD-LOGIC uses a special prefix #:
" to indicate that a symbol
is not equal to any other syntactically different symbol with the #:
prefix and not equal to any numbers or lists.
For example, both ["#:pete","=","#:john"]
and "["#:pete","=",2]
must be evaluated to false, while ["pete","=","#:john"]
and
["pete","=",2]
are not evaluated to false.
The distinct symbols can be seen as an extension of the string type:
a string function "$strlen"
and predicates "$substr", "$substrat"
are defined in JSON-LD-LOGIC for the distinct symbols.
The distinct symbols of JSON-LD-LOGIC are translated to the distinct symbols of the TPTP language with the same semantics as described above. In the TPTP language the distinct symbols are surrounded by double quotes.
[
{
"@id":"smith1",
"@type":["#:person","baby"],
"name":"John Smith"
},
{
"@id":"smith2",
"@type":["#:dog","newborn"],
"name":"John Smith"
},
["if",
{"@id":"?:X","@type":"?:T1"},
{"@id":"?:Y","@type":"?:T2"},
["?:T1","!=","?:T2"],
"then",
["?:X","!=","?:Y"]
],
{"@question": ["smith1","!=","smith2"]}
]