Example 1 for json basics

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.

[
["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"]].
• Strings prefixed by ?: 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.

Example 2 for more connectives

We use the equivalence "<=>", 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"]]]
]
  
  

Example 3 for answers

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.

Example 4 for free variables and syntactic sugar

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"]]
]

Example 5 for equality

Predicates "=" 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"]]
]

Example 6 for the grandfather with equality

This example reformulates the grandfather relation using equalities.

[
["=",["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"]]
]

Example 7 for json-ld basics

JSON-LD objects aka maps are interpreted as logic and can be mixed with the core fragment constructions written as lists in the previous examples.

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"]}
]

Notice that

• The proof replaces json object/map constructions by the list constructions using the $arc predicate.
• The value of the "@question" key is transformed to [["$arc","?:X","grandfather","john"], "=>", ["$ans","?:X"]].
• The name "gfrule" is used in the proof.

Example 8 for json maps in logic and if-then

Exactly as the previous example, but using objects/maps inside the "@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"}}
]

The proof is identical to the proof of the previous example.

Example 9 for the json-ld context

An important feature of JSON-LD is the use of the "@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"}}
]

Notice how the JSON-LD namespace rules in "@context" transform the property names. The same property names outside the "@context" scope have to be presented as absolute values in a long form.

Example 10 for nested objects and arithmetic

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:

• Type detection predicates "$is_int", "$is_real".
• Comparison predicates "$less"`, `"$lesseq"`, `"$greater"`, `"$greatereq".
• Type conversion functions "$to_int"`, `"$to_real".
• Type conversion functions "$to_int"`, `"$to_real".
• Arithmetic functions on integers and reals: `"$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"}]}
]

A new unique blank node "_:crtd_..." is built for each object/map without an explicit "@id" key.

Example 11 for named graphs and quads

JSON-LD uses the "@graph" key for two objectives:

• If an object does not contain an "@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.
• If an object does contain an "@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"}}
]  

Example 12 for the list datatype

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"}}
  
]

Example 13 for distinct symbols

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"]}
]