Logic 16 Tool

[Shima Costar]

Gkc defines a function and three predicates on distinct symbols:

• $strlen(S) returns the integer length of a distinct symbol S as a string.
• $substr(A,B) evaluates to true if a distinct symbol A is a substring of a distinct symbol B, and false otherwise, provided that A and B are distinct symbols.
• $substrat(A,B,C) evaluates to true if a distinct symbol A is a substring of a distinct symbol B exactly at the integer position C (starting from 0), and false otherwise, provided that A and B are distinct symbols and C is an integer.
• $is_distinct(A) evaluates to true if A is a distinct symbol and false if A is a number or a list.

Automated reasoning Automated reasoners prove logical theorems, answer questions and (sometimes)can detect unprovability. Basically, they are highly optimized search systemsoften encompassing a large number of different search strategies.Most of the reasoners are specialized to performwell on some specific kinds of problems or are extended with additionalspecial capabilities. For example, the gkc prover used in this siteis specialized for very large problems, although this capability cannot be used well in the confined browser environment. Hint: you may want todownload the command-line version for more advanced use.A large special category of provers focuses on propositional logic. See the Propositional logic menu for checking out theircore ideas. The easiest way to find top level propositional solvers is to check the The international SAT Competition: youwill see the competition results for various problem categories, can download competitionproblems, source code and descriptions of the provers.A good alternative choice is to check out minisat: an easily extensible and hackable state of the art solver which is a basis for severalother state of the art solvers. You can runcrypto-minisat in your browser,compiled from C to javascript using LLVM.Good reading material for predicate logic provers:

• AutomatedTheorem Proving Course Content by Geoff Sutcliffe is probably the best introductory material
• Implementation tutorial by Stephan Schulz
• A detailed theoretical coursebook by Marek Kosta and Christoph Weidenbach
• Handbook of Practical Logic and Automated Reasoning contains code examples in ML in additionto an excellent text
• Handbook of Automated_Reasoningfor in-depth papers(here on Amazon).

For experimenting with general-purpose predicate logic solvers check out:

• The TPTP Problem Library for Automated Theorem Proving by Geoff Sutcliffe and Christian Suttner.
• Online solvers on TPTP
• The CADE ATP System Competition
• PyRes A well-documented simple implementation in Python for illustrating the basic machinery.Several specialized categories of predicate logic solvers exist in addition to the general-purpose solversmentioned above. Some of the categories are:
  • Interactive theorem proverslike Lean, HOL, Mizar, coq.
  • SMT (satisfiability modulo theories) solvers used forformal verification likeZ3and PVS
  • Answer set based solverslike DLV andSmodels, seethe competition
  • Description logic solvers, see the list of implementations
  • OWL (web ontology language) solvers used in the context of semantic web, see the list of implementations

Why the negation and contradiction? This is just a convenient way to simplifythe problem. Here we really want to prove a & b => a. This is trueif 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, givinga 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 reallyspecial about it.

Notice that each statement in the input file is terminated with a period sign.The list of statements is assumed to be a conjunction (and) of all statements. Minus sign - means negation. Thus -father(john,pete) means john is NOT the father of pete.

The order of statements is not really important, although it may cause minorand essentially unpredictable differences in search behaviour. Essentially, gkccreates and tries out its own search strategies, like SQL databases. It does notfollow a pre-determined predictable search strategy like PROLOG.

The [mp, 1, 2] (not exactly present in this proof) means that this fact / rule 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 andthe rest were glued together.

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, the following examples are understandable without in-depth theoretical background.

Although the task is trivial, gkc does not attempt to be clever and tries out a large numberof search strategies: this is why it takes a second to terminate. You can try running gkcwith the optional switch producing more information to see the whole process: clickon the Advanced button and select a higher print level or set the Show derivedto on

We are using a variable here: any word starting with a capital letter is consideredto be a variable. X is a variable in our example. You could also use, say Somethingas a variable: it also starts with a capital letter. All the words starting witha non-capital letter are constants, functions or predicates.

The [mp, 1.2, 2, fromaxiom] means that the 2th (numeration 0,1,2,...) literal in the clause at proof step 1 was cut off with the first (0th) literal of the clause at proof step 2. In case the first literal is cut off,the N.0 is simplified to N, as in the previous examples.

father(john)=pete means, as expected, that pete is the fatherof john and there can be no other fathers. If you also gavefather(john)=lucas this would make gkc to conclude thatpete and lucas are the same object, i.e. pete=lucas.

Importantly, two different constants are not considered inequalby default (think of the constants as labels on objects: there couldbe several different labels on one object):a=b does not give a contradiction.

See that gkc was happily answering father(mark) although we havenot said who the father of mark actually is! The functions like father do not have to be defined on all the possible objects, they can be partiallyknown and partially unknown.

The "strategy": ["negative_pref"] indicates that one specificstrategy (here a conventional negative-preference ordered binary resolution)is to be used for proof search, without any parallel or sequential attemptswith different search strategies.

The proof uses given equalities to derive several new equalities.The = rule basically replaces parts of one premiss matching (unifying)one side of the second premiss equality with the other side of the equality.

It is a good idea to click on the Advanced button and enter a sensibletime limit to the Seconds box.p(a).-p(X) p(f(X)). Example with a hard problemAs an example of a small but a really hard problem for gkc which isnevertheless actually provable, try the problem LCL876+1from the TPTP collection.It will probably run until the browser complains badly or time given by the automatic strategy selection runs out.

The goal is to find a sequence of robot arm movements to producea required configuration of blocks: for example, a tower. The commentsin the problem text explain the initial situation and the arm movementrules.

You can put whitespace or any symbol (single quotes inside quotedsymbols must be prefixed by a backslash) into symbols by surrounding the symbol with single quote symbols like this: 'John \'Smith\'!' which is treated as a constant, despite thatit starts with a capital letter inside the quotes.Any symbol containing a character except an ascii letter, digit, underscore _,or dollar $ will be printed out by surrounding it with single quotes.As an exception in gkc, equality = and conveniece infix forms ofarithmetic expressions +, *, -, /, will not be surrounded by quotes.

Double quotes like "John Smith" indicate thata symbol is distinct, i.e. unequal to any other distinct symbol,number or a typed object. Double quotes inside double quoted symbols mustbe prefixed by a backslash. More about distinct symbols in the later examples.

Additionally gkc allows to make a symbol variable by prefixing it with a questionmark like this: ?smth. Any symbol starting with a capital letter or a question mark is assumed to be a variable, and the rest are not.

Thus, for gkc in fof formulas a capital-letter-starting symbol is a free variable even ifit is not explicitly quantified: since this could be confusing, itmay be better to avoid such symbols unless they are explicitly quantified.

This example is a classic "Schubert's Steamroller" puzzle taken fromTPTP and written in fof syntax with connectives like implication as =>, quantifiers for all as ! [X] ..,, exists as ? [X] ... etc. The full list of infix binary connectives follows the TPTP language:

• "" for disjunction,
• "&" for conjunction,
• "" for equivalence,
• "=>" for implication,
• "

Gkc will first convert the complex formulas to a simple clause form (properly calledclause normal form) used in the previous examples. The statements we had in theseexamples are called clauses.

where the statement name will be used in the proof, the statement role indicates whetherit is an axiom, an assumption or hypothesis, or a goal to be proved from these: the latter is eitherconjecture (which has to be negated) or negated_conjecture (negated already).

The first formula in the example is universally quantified (! symbol)and will be converted by gkc to a clause -wolf(X) animal(X)..The second statement is existentially quantified (? symbol) and will be converted by gkc to a clause wolf($sk7).where $sk7 is a new constant invented by gkc which should not occur in any other formula in the problem:this procedure is called Skolemization.Gkc always uses the $sk prefix for such constants and functions, using a new number Nfor each new one. The original formula is assumed not to contain $skN form symbols.

c80f0f1006