Example 1: facts, rules, a default

Each statement ends with a period. Lowercase names such as pingu are constants and predicates; uppercase names such as X are variables. bird(X) :- penguin(X) is a rule: every penguin is a bird. A minus sign states a negation, so the next rule says a penguin does not fly.

The last rule is a default: a bird flies unless -flies(X) can be argued — the classical "birds normally fly" with its exception. An unless may also carry a numeric priority, as the later default examples do; without one the default is simply incomparable with explicitly ordered defaults, which this example does not need. The query statement asks the question; since it contains the variable X, gk returns each value for which flies(X) can be derived.

A percent sign % starts a line comment; /* ... */ comments work as well. The order of statements does not matter.

tweety flies with confidence 1: the default applies and no argument for its exception is found. The blockers line records the exception the answer depends on. pingu is shown as a rejected answer: the flying default produced a candidate, but the strict penguin rule proves -flies(pingu) and defeats it — the rejected block shows both the candidate's proof and the proof against it.

Each proof block lists numbered derivation steps. in(frm_1) marks an input statement; mp(1.1, 2) means the step was derived from steps 1 and 2 by resolution (the decimal names the literal used). The number after each step name is the stored support value at that step.

The internal literal $ans(X) collects the answer value: the last step of tweety's proof contains $ans(tweety).

Example 2: confidences

A number between 0 and 1 before :: is an input confidence. Facts and rules can both carry confidences. A statement without the prefix has confidence 1.

Both facts and rules can be uncertain. gk computes support for the answer from the confidences of the inputs used in the proof.

The answer is true with confidence 0.56 = 0.8 * 0.7. A proof chain multiplies the input confidences of the statements it uses, under the assumption that their uncertainties are independent.

Example 3: several sources

Two independent sources support the same forecast with different confidences. Their combined support is greater than either confidence alone.

The combined confidence is 0.8. For independent evidence gk combines the two proofs as 1 - (1 - 0.5) * (1 - 0.6) = 0.8: the answer fails only if both sources fail. This is the same "noisy-or" rule used in probabilistic logic programming.

The proof shows both derivations and a cumul step which merges them. Importantly, gk records the ground evidence instances used by each proof and accounts for shared instances during the merge: see the "shared evidence" example.

Example 4: positive and negative support

The minus sign is explicit negation: -flies(tweety) is evidence that Tweety does not fly, not an absence of evidence. Here both the statement and its negation have direct support. gk retains and assesses both polarities.

The detailed report option (in Advanced) is switched on for this example: it adds a breakdown of the evidence to the answer.

The answer true has confidence 0.3: the positive support 0.7 minus the part 0.4 contested by the negative support.

The detail lines split the total belief into four parts which sum to 1:

support: 0.3 for, 0 against
conflict: 0.4   ignorance: 0.3

Positive support and negative support are the unopposed components. Conflict is the component claimed by both polarities, and ignorance is claimed by neither. The CONTESTED flag warns that the answer has real negative support, not merely weak positive support.

Both the proof for and the proof against are printed, so you can see exactly what supports each polarity.

Example 5: rule chains

Uncertain rules with variables act as weak general tendencies: the base smoking rule has confidence 0.3, the friendship rule has confidence 0.1, friendship is roughly symmetric, and the smoking-influence rule has confidence 0.2. On top of these there are two certain facts about chris and sam.

The question is how strongly the rules and facts together support smokes(sam).

The confidence is 0.3764. Several different derivations support the answer: the base tendency (0.3), and a chain through the friendship — sam may be susceptible (0.6), sam is a friend of chris, chris smokes. The friendship itself pools two sources: the known fact via the symmetry rule (0.9) and the general 0.1 tendency, 1 - (1 - 0.9)(1 - 0.1) = 0.91. The chain then contributes 0.6 * 0.91 * 0.2 = 0.1092, and the noisy-or with the base tendency gives 1 - (1 - 0.3)(1 - 0.1092) = 0.3764. gk finds the separate proofs and cumulates them, multiplying rule confidences along each chain and combining the chains with the noisy-or rule, without counting the shared friendship evidence twice.

The cumul steps in the proof show where alternative derivations are merged.

Example 6: shared evidence

Two rules predict rain: one from dark clouds and falling pressure (support 0.72), another from dark clouds and the radar (support 0.63). Combining the two proofs naively as independent supports would give 1 - 0.28 * 0.37 = 0.896.

But that would be wrong: both proofs stand on the same uncertain observation dark_clouds(today). If the cloud observation fails, both proofs fail together, so the two are not independent.

gk returns 0.846, not 0.896. It records which input facts each proof uses, notices that dark_clouds(today) is shared, and combines only the non-shared parts independently: 0.9 * (1 - (1 - 0.8) * (1 - 0.7)) = 0.9 * 0.94 = 0.846.

Replacing dark_clouds(Day) in the second rule with an independent observation with confidence 0.9 would remove the overlap and change the result to 0.8964.

Example 7: contested premises

Here the conflict is not about the queried statement itself but about a premise used to derive it: bird(tweety) has positive support 0.5 and negative support 0.2.

The detailed report is switched on to show how gk flags this.

The conclusion gets confidence 0.27: the flying rule (0.9) applied to the support of its premise that survives the opposing evidence. The flags: CONTESTED line marks that a premise of the proof has opposing evidence. That opposition need not appear in the printed answer proof: gk finds it with the separate directed search over the input clauses.

JSON detail output can also list contested atoms as conflict_sources; see the "conflict detail" example under more examples.

This example is also a good one for the sampling check under Advanced, because its modes pull in different directions. Reading each input confidence as an independent activation probability and counting the worlds in which flies(tweety) is provable gives about 0.45 (a finite sample lands nearby, for example 0.46), not 0.27: that count includes every world where the bird premise holds, even the worlds where "tweety is not a bird" holds alongside it, so the negative support for the premise changes nothing. The shared threshold mode instead arrives at gk's own 0.27, and not by accident: there the two bird statements compete for one shared acceptance threshold, so the premise counts only in the 0.5 - 0.2 = 0.3 margin between them — the same subtraction gk computes — and the flying rule fires in 0.9 of that. The difference between the first reading and gk is genuine; see checking by sampling above.

Example 8: defaults

The unless(-flies(X), 2) condition makes this a default rule: derive flies(X) from bird(X) unless an argument for -flies(X) blocks it. The number 2 is the priority of the default, used when defaults compete; see the later examples.

This states that birds normally fly without claiming that every bird flies.

Both tweety and robin are answers with confidence 1: there is no support for either negation, so the defaults go through.

Each answer records its blockers — the exception condition it depends on, e.g. unless(-flies(robin), 2). The answer is conditional on no such blocker being derivable: gk searched for evidence of the exceptions and found none.

Try adding the fact -flies(tweety). and solving again: tweety disappears from the answers, robin remains.

Example 9: an exception

The new fact 0.9::-flies(tweety) supports the default's exception condition and the negation of its conclusion, with confidence 0.9 rather than 1.

robin still flies with confidence 1. For tweety, negative support 0.9 for the exception condition exceeds the default's surviving positive support: tweety is shown as a rejected answer with confidence against 0.9 - 0.1 = 0.8. The default holds only in the one case in ten where the contrary evidence is absent, so 0.1 supports flying and 0.9 supports the opposite.

The output shows both the proof for (the default) and the proof against (the exception evidence) for tweety.

Try changing 0.9 to 1: with a certain exception the rejection is complete, with confidence against 1.

Example 10: penguins

Two default rules compete: birds fly (priority 3) and objects do not fly (priority 2). Since every bird is an object, both defaults apply to every bird. The higher priority number wins, so for ordinary birds the flying default defeats the non-flying one.

The penguin rule -flies(X) :- penguin(X) has no unless: it is strict, and strict conclusions override any default.

The bird tweety flies with confidence 1: its priority-3 default defeats the priority-2 object default (the printed proof against shows the defeated attempt).

The penguin pingu is printed as a rejected answer with confidence against 1: the flying default produced a candidate, but the strict penguin rule defeats it regardless of priorities.

The rejected-answer block records the defeated candidate and its opposing proof.

Example 11: the Nixon diamond

Two defaults of equal priority support opposite conclusions about the same person: the quaker rule supports pacifism and the republican rule supports its negation.

The query asks about a further consequence of pacifism.

gk reports result: evidence below limit and shows nixon only as a rejected answer with confidence against 0 and the CONTESTED flag. Neither default can defeat the other — the priorities are equal — so the margin between them is zero: gk commits to neither pacifist(nixon) nor its negation, and the downstream conclusion is left undecided (ignorance 1 in the detail lines).

Try raising the quaker default to priority 3: then pacifism wins and nixon becomes a real answer with confidence 1.

Example 12: where is John

Three movements happen one after another: John to the hallway, Mary to the bathroom, John to the kitchen. Where is John at the end?

The point is what happens between the movements: nobody restates where John is while Mary moves, so his location must persist on its own. The last rule states this as a default with confidence 0.99: a location carries over to the next situation unless that person moved. Defeat of persistence by known events is the classical frame problem handled with defaults.

The answer is kitchen with confidence 1, straight from the movement rule.

hallway appears as a rejected answer: John's hallway location persisted through Mary's movement into s2 (nobody named John moved then), but his own move from s2 to s3 establishes moved(john, s2), which defeats the persistence default for that step. The rejected block shows the whole persistence chain with its two unless blockers.

Steps such as mp(1.1, 4) use a decimal to name which literal of the earlier clause was resolved: the first literal of step 1.

Try deleting only the line move(john, kitchen, s2, s3)., keeping next(s2, s3).: then hallway becomes a real answer at 0.99 * 0.99 = 0.9801, the persistence default applied twice. (Deleting the next line as well would remove the transition to s3 altogether, and the query would have no answers.)

Example 13: arithmetic

Ground arithmetic (3 + 4 < 10 etc) is evaluated during proof search. To find a value for a variable in an arithmetic condition, gk uses bounded enumeration of candidate values. Automatic selection enables this when required; the preset strategy shows the corresponding arith_instantiation setting.

The answer is 7 with confidence 0.8 (the rule's own confidence). The proof shows the instantiation step where Boxes = 7 makes 7 * 6 = 42 true.

This is bounded search for satisfying values, not equation solving: it handles one unknown conservatively (arith_instantiation: 1), and mode 2 also tries selected two-variable cases. The rule encodes exact equality, not capacity: with 43 books no value of Boxes satisfies it, and there is no answer.

Example 14: equality reasoning

The first fact defines a function value: the capital of Estonia is Tallinn. The second states that Alice lives in the capital of Estonia. The question uses the other name of the same city.

gk handles equality with dedicated inference rules (paramodulation), the same machinery used by classical theorem provers: the term capital(estonia) is rewritten to tallinn wherever it helps a proof.

The answer is true with confidence 1. The = step in the proof is an equality replacement: capital(estonia) inside the second fact is rewritten to tallinn, after which the question matches directly.

Example 15: conflict sources in detail

Several sources give evidence about whether tweety is a bird — two positive sightings and one negative report. One rule supports flying from birdness; the other supports not flying from evidence that something is not a bird. The detailed report (switched on for this example) names which atom the conflict comes from. Note that input confidences can also be written as percentages: 90 means 0.9.

The answer has confidence 0.252 and its detail block lists

"conflict_sources": [{"atom": ["bird","tweety"], "conflict": 0.7000}]

naming the contested premise and the size of the conflict on it: the two sightings of bird(tweety) cumulate to 0.98, the doubt claims 0.7 of that mass. The CONTESTED flag and the conflict-source list identify the affected premise.

Example 16: JSON notation

The weather example is written in gk's JSON-LD-LOGIC notation. The input is a JSON list, variables start with ?:, and keys such as @confidence and @question attach metadata.

This notation is intended for logic generated or consumed by programs.

When the input is JSON, the output is JSON as well: machine-readable answers with the same proofs as in the text format. Confidence 0.56 matches example 2 because the two inputs encode the same statements.

Example 17: GKS notation

The third input notation: rules are written premises-first with & and =>, closer to textbook logic than the Prolog-style :- form. Everything else — confidences, queries, unless — is the same.

gk detects the notation automatically from the input text, so all the notations work in this same text box.

The answer is true with confidence 0.56, as in examples 2 and 16. All three inputs are translated to the same internal logic before proof search.

Example 18: TPTP notation

gk also reads clause-normal-form problems in the TPTP notation used by automated theorem provers, extended with a confidence(...) annotation in the optional useful-info list of the cnf(...) form (the field after the source position). This example asks which object does not fly: extracting a value for the open variable is a gk convention layered on top of TPTP clause form, not part of TPTP semantics itself.

With TPTP input the answer comes back in the TPTP style: an SZS status line, the answer tuple, and the proofs as inference lists. The penguin p is the answer at confidence 0.72 - 0.08 = 0.64: the no-fly rule applies through the 0.8 penguin fact (0.8 * 0.9 = 0.72 for not flying), while the flying default supports the opposite only in the 0.08 where the penguin is a bird but the no-fly rule does not apply.

The output notation follows the input notation.

This example rewards a look with the sampling check under Advanced: counting the worlds in which -flies(p) is provable, minus those in which flies(p) is, gives about the same 0.64; see checking by sampling above.

Example 19: defaults in JSON

The birds-and-penguins default in JSON notation. What GKP writes as unless(-flies(X), 3) appears here as an explicit $block literal inside the rule clause: ["$block", 3, ["$not", ["flies", "?:X"]]]. The GKP and GKS unless forms are translated to exactly this.

b1 flies (confidence 1); the answer lists its $block blocker just as the text format lists blockers:. Programs generating JSON-LD-LOGIC use this form directly.

Example 20: blocks-world planning

A classical planning problem: blocks on a table, a robot arm, and a goal configuration. The plan is found as the answer term: a nested sequence of pickup/putdown actions transforming the initial situation.

The time limit is preset to 30 seconds and max answers to 1 (one plan). The search runs off the page's main thread, so the page stays responsive; press Stop to abort it.

The answer is a situation term: read it inside-out, starting from s0, as the sequence of actions of the plan. Decoded, the returned plan is:

1. pick up b
2. put b on a
3. pick up c
4. put c on b

Finding the first plan takes several seconds.

Example 21: logic generated from English

The input was machine-generated by the llmpipe pipeline, which uses a large language model to translate English to gk logic: the story is "Penguins are birds. Penguins cannot fly. Birds can fly. John is a penguin. John flies?". Each clause carries its source sentence in the @nl field. The pipeline numbers each named entity, so #:John 1 is the generated identifier for the first entity named John (the #: prefix marks a unique object) — not a typo in the input.

The encoding uses events with actors and types rather than a simple flies(john) atom, so that the same scheme covers arbitrary verbs, and a shared background knowledge base (loaded automatically for this example, not visible in the text box) supplies general axioms for taxonomy, part-whole relations, degrees, events and space. The displayed clauses are the generated ones; only the background axioms are added behind the scenes.

The $ctxt terms carry the context an atom is asserted in — tense, world, location and knowledge source — so that the background axioms can reason about when and where a statement holds. They are part of the llmpipe encoding scheme, not something gk requires.

The expected answer is false: John, a penguin, does not fly. The "birds can fly" sentence became a default (note the $block in its clause and its 0.9 confidence) which the strict penguin sentence defeats, exactly the penguin pattern from the earlier examples — only now produced automatically from English text.

Example 22: a which-question from English

A wh-question produced by the same llmpipe English-to-logic pipeline; the displayed clauses are the generated ones, with the shared background axioms loaded behind the scenes. The answer value comes back wrapped in $ans: a name like #:John 1 is a specific individual mentioned in the text, while a value like $some_fox is an existential one — "a fox", introduced by the text without a name. The $ctxt terms carry the context an atom is asserted in (tense, world, location, knowledge source), as in the previous example.

The answer is $some_fox, with confidence 1: an unnamed fox introduced as a representative member of its class. Population clauses (marked @sourcetype: "populate") supply such typical members for the classes mentioned in the text, so that questions about "a fox" or "some bird" have witnesses to find.

Example 23: taxonomy classification

Three objects with known parts: h1 has a leg, b1 has a leg, a wing and feathers, a1 has an engine and a wing. Uncertain default rules classify by parts; the question asks which objects are organisms.

The defaults here use tax(class) instead of a numeric priority: the priority is looked up from a WordNet-derived taxonomy, in which a more specific class defeats a more general one. The taxonomy comes from two data files (a mapping of names to class numbers and the packed class hierarchy), fetched gzipped (about 0.9 MB) and loaded automatically for this example; gk then runs with its -defaults option.

b1 is an organism with confidence 0.5552: the bird evidence from leg, wing and feathers cumulates to 0.936, the independent human evidence (0.3, from the leg) joins it — 1 - (1 - 0.936)(1 - 0.3) = 0.9552 — and the opposing airplane default (0.4, from the wing) subtracts from that: 0.9552 - 0.4 = 0.5552. The answer is reported through both its human-default and bird-default derivations, with the tax(...) blockers listed. Each block is one derivation family, and every block is headed by the same aggregate confidence — not by the share contributed by the proof shown inside it.

h1 follows with confidence 0.44: the human (0.3) and bird (0.2) leg-defaults cumulate to 1 - 0.7 * 0.8 = 0.44.

a1 is a rejected answer with confidence against 1: the wing suggested a bird, but the strict rule that nothing with an engine is an organism defeats the default regardless of taxonomy priorities.