About this site

The goal is to help studying logic and solvers by providing easy-to-use, pure browser-based javascript tools for both full classical predicate logic and propositional formulas.

The high-performance predicate logic prover gkc is written in C and available available under the AGPL v3 licence as a command line tool on Linux, Windows and macOS and Wasm for running in the browser. The browser version on this site is inevitably crippled when compared to the command-line version: the latter can utilize multiple cores, all the available memory, shared memory databases and has several additional options not available in the browser. The browser version runs on a single core and has severe memory restrictions.

The educational propositional provers are self-contained, no-dependencies, easy-to-hack javascript code under the MIT licence. The focus is on simplicity, ease of use, hacking and experimenting, not state of the art efficiency-wise.

Help and cooperation appreciated for improving the current code, writing and proposing new tools, etc. See the github page.

Contact the author Tanel Tammet as (tanel.tammet at gmail.com).

What is this?

A toolkit for proving classical first order predicate logic and propositional logic formulas, answering questions and converting between different syntaxes for logic.

Think about logic as a generic way of writing rules: proving formulas and answering questions is a way of detecting what follows from the rules we wrote.

The predicate logic toolkit is built around a high-performance reasoner gkc (see the paper) and runs in the browser using Wasm without any server involvement. For more advanced use you may want to download the command-line version.

The educational propositional provers are self-contained, no-dependencies, easy-to-hack javascript code under the MIT licence. The focus is on simplicity, ease of use, hacking and experimenting, not state of the art efficiency-wise.

Use these tools for learning logic and experimenting with reasoners.


Basic predicate logic syntax

A good way to learn syntax and meaning is to go through the explanations in the simple examples. Nevertheless, the following presents a compact description.

Gkc supports several syntaxes: the simple syntax used in most examples, TPTP syntax and JSON-LD-LOGIC syntax: see the separate Json menu for the examples and explanations.

The simple syntax is an extension of the TPTP FOF and CNF syntaxes as described in the TPTP technical manual, combining them into one and extending with a list type and a few convenience predicates and constructions.

The simple syntax input is a list of logical formulas, each terminated with a period. The whole list is interpreted as a big conjunction (and) of formulas.

Each formula is either a literal (a positive or a negative atom) or is constructed from simpler formulas using logical operators like

  • & for conjunction (and),
  • | for disjunction (or),
  • - or ~ for negation (not),
  • => for implication (if-then),
  • "for all values of variables holds ..." construction ! [variables] : formula (example ! [X,Y] : p(X,Y))
  • "exist values of variables so that ..." construction ? [variables] : formula.

Additional logical operators will be described later.

An atom is a predicate symbol applied to a number of term arguments like father(john,pete) and denoting a relation between the arguments. A negated atom has a minus sign prepended like -father(john,pete).

Equality is a special predicate written like gender(john)=male and meaning, as expected, that the term on the left side is equal to the term on the right side. Inequality is another special predicate written like gender(john)!=female

The terms denote objects. A simplest term is just a symbol/constant like john: think of it as a post-it note glued to some real thing or idea: a real object may have many such notes glued to it. A variable like X is also a term: think of it as placeholder which can be replaced by any other term.

Variables must start with an upper-case character, other symbols with a lower-case character. There are also other options for symbols, more about these below.

A variable which is not in the scope of a for all ! or exists quantifier ? is treated as if it is bound by the for all quantifier. In fact, explicit quantifiers can be skipped altogether: they are just a convenience construction.

Numbers like 12 or 3.45 can be also used as constant terms.

More complex terms can be constructed from simpler terms using functions like age(mother(john)) or $sum(X,$multiply(2,X)). A value of such a function is not always defined: it can be used just as a constructor for complex terms. A function may also be defined on some other terms, like $sum is defined on numbers, but not on lists. You may define functions yourself using equality like mother(john)=eve or age(mother(john))=age(mother(pete)).

Both line comments % and multi-line comments /* ... */ are available.

What does it mean?

Logic can be seen as a fairly general way of writing down facts and rules, while proving the formulas means detecting what follows from the rules.

Think about an atom like father(john,pete) as saying that there is a row with two cells john,pete in a two-column table father. In fact, the core ideas of relational database systems and SQL stem from this interpretation, although they branch off into specific directions. For example, in conventional logic notation all the elements in row columns are given positionally, one after another, while in SQL columns have names.

Each predicate like father should be seen as giving rise to two different tables: one for positive facts and another for negative facts: -father(john,mike) means that in the negative -father table there is a row john,mike. Importantly, the facts we state only say that there are these-and-these rows, but they do not say that there cannot be other rows, unknown to us. This inpreretation is called open world assumption contrasting the closed world assumption used in database systems and Prolog.

Logical formulas are then understood as rules for deriving new rows in the tables. For example. father(X,Y) => child(Y,X) means that if there is a row in the father table, the corresponding row with arguments exchanged must be put into the child table.

A rule like -father(X,X) can be seen as saying that the negative -father table contains rows like object_n,object_n for all objects. Since we could potentially have infinitely many objects (think numbers and terms constructed from functions) we cannot always physically fill in all the rows.

A contradiction occurs when a row in the positive table also occurs in the corresponding negative table. For example, saying father(john,john) would contradict the row john,john in the negative -father table, given the rule -father(X,X).

Finding a contradiction is used as one convenient way of finding whether some fact/row follows from our rules. Suppose we have two statements father(john,pete) and father(X,Y) => child(Y,X) and we want to prove an obvious fact that child(pete,john) follows from these two. Let us denote these three statements as a, b, c. Then we really want to prove that a & b => c is true, which is equivalent to the question of whether the negated form -(a & b => c) is contradictory, which is equivalent to the question of whether the conjunction a & b & -c is contradictory. Hence we could add the negated form -child(pete,john) to our two initial statements and check whether a contradiction can be found.

Finally, an important principle of logic as used here is that no common knowledge - or rather, no knowledge at all - is assumed. Everything we want to use must be written explicitly as logical facts and rules. The names of the predicates mean nothing in itself: a reasoner knows nothing about the father predicate except what is explicitly written in the problem statement. You could replace all the nice human-understandable names with meaningless names and the logical meaning of the problem statement would be exactly the same.

Special symbols and additional constructions

Ordinary symbols must start with lower-case character and must not contain any whitespace or non-alphanumeric characters like (, -, ~, =, " etc: however, underscore _ and dollar $ are allowed.

You can put whitespace or any symbol except a single quote into symbols by surrounding the symbol with single quote symbols like this: 'John Smith'. Internal quotes must be prefixed by a backslash \.

Additionally you can make a symbol variable by prefixing it with a question mark like this: ?smth.

Double quotes surrounding a symbol like "John Smith" have a special meaning: the symbol is treated as distinct (essentially, a string) meaning that it is known to be unequal to any syntactically different distinct symbols, numbers and lists. This has real effect for equality and string predicates, but not otherwise.

In addition to the typically used constructions &,|, -/~, =>, !, ? the syntax provides a number of additional infix logical constructions with two arguments. The full list is:

  • | 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.
There are several predicates and function symbols with a pre-defined meaning: all these are prefixed with a dollar $.

$ans is used for finding the actual terms we look for as answers: see the answers example.

Arithmetic in predicate logic

The numbers and arithmetic functions and predicates are defined following the TPTP arithmetic system plus a few convenience operators for writing infix terms:

  • Type detection predicates $is_int, $is_real.
  • Comparison predicates $less, $lesseq, $greater, $greatereq.
  • 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.

    Note: these comparison predicates and arithmetic functions take exactly two arguments.

    Example: $less($sum(1,$to_int(2.1)),$product(3,3)).

  • Additional convenience predicate is used: $is_number is true if and only if $is_int or $is_real is true.
  • Additional infix convenience functions +, -, *, / are used with the same meaning as $sum, $difference, $product and $quotient, respectively.

    Example: $less(1+(1+2),(3*3))

    Note: these convenience functions take also exactly two arguments.

NB! Do not use a variable or a non-numeric constant as a first element of the infix arithmetic expression like p(X*2), otherwise the whole expression will be parsed as a single variable X*2. No such restrictions apply for the prefix form.

Lists in predicate logic

You can use the list syntax like [] for the empty list and [a,b,c] for a three-element list. The bracket notation is syntactic sugar for the constant $nil and functional list-constructing term $list(a,$list(b,$list(c,$nil))), respectively.

Observe that $list(X0,X1) constructs a list by prepending X0 to the list X1, which is generally different from a two-element list [X0,X1].

Terms constructed using $list or $nil are interpreted as having a list type:

  • A list type object is inequal to any number or a distinct symbol.
  • Syntactically different list type objects A and B are unequal if at any position the corresponding elements of A and B are unequal typed values: numbers, lists or distinct symbols.
The following predicate and two functions are defined on lists:
  • $is_list(L) evaluates to true if A is a list and false is A is a number or a distinct symbol.
  • $first(L) returns the first element of the list.
  • $rest(L) returns the rest of the list, i.e. the result of removing the first element.
These functions can be applied to non-list arguments, where they are left as is and not evaluated.

Distinct symbols as strings

Symbols in double quotes like in "person" stand for for distinct symbols which can be viewed as a string type. A distinct symbol is not equal to any other syntactically different symbol and not equal to any numbers or lists.

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 for predicate logic

Automated reasoners prove logical theorems, answer questions and (sometimes) can detect unprovability. Basically, they are highly optimized search systems often encompassing a large number of different search strategies.

Most of the reasoners are specialized to perform well on some specific kinds of problems or are extended with additional special capabilities. For example, the gkc prover used in this site is specialized for very large problems, although this capability cannot be used well in the confined browser environment. Hint: you may want to download 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 their core ideas. The easiest way to find top level propositional solvers is to check the The international SAT Competition: you will see the competition results for various problem categories, can download competition problems, 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 several other state of the art solvers. You can run crypto-minisat in your browser, compiled from C to javascript using LLVM.

Good reading material for predicate logic provers:

For experimenting with general-purpose predicate logic solvers check out: Several specialized categories of predicate logic solvers exist in addition to the general-purpose solvers mentioned above. Some of the categories are:

What is the practical use?

For the generic reasoners, mostly niche applications so far. The eighties-hype of expert systems and symbolic A.I. with little practical value lead to the famous A.I. winter. This said, the propositional and SMT provers are seriously used for verification, test generation and configuration management.

The main obstacles for wider use: (a) it is very hard, or practically impossible (although theoretically possible) to hand-encode most of human expert knowledge in logical rules, (b) proof search without intelligent guidance is really hard, (c) basic predicate logic without probabilities, default reasoning etc etc is extremely impractical for encoding commonsense knowledge.

There is hope for a new rise of reasoners as parts of a machine-learning-and-reasoning hybrid systems performing common sense reasoning. Check out a preprint proposing several mechanisms in this direction.

Propositional logic syntax

Use either a conventional formula syntax like

(a -> b) & a & -b
or a dimacs version of the clause normal form syntax like
-1 2
which is a conjunction of disjunction lines with numbers standing for variables: the last example means simply (-x1 v x2) & x1 & -x2

For conventional formula syntax:

  • negation symbols are -, ~
  • conjunction symbols are &, and
  • disjunction symbols are |, v, V, or
  • xor symbols are +, xor
  • implication symbols are ->, =>
  • equivalence symbols are <->, <=>
There is no operator precedence; all operators are bound from left:
a & b v c & d v e is read as ((((a & b) v c) & d) v e)

For dimacs you may use or skip the initial comment lines starting with c, the special p line and the final 0 symbols at the end of each disjunct. We allow the trailing 0-s only at the end of a line.

I.e. you may use the full dimacs version like

c comment
p cnf 2 3
-1 2 0
1 0
-2 0
or just

-1 2

What does it mean?

Solving a classical propositional formula means looking for such values of variables that the formula becomes true. For example, (a -> b) & a becomes true if and only if both a and b are assigned true.

You can select and try out several solver algorithms: the "DPLL better" is the best solver amongst the options offered on our page. Read the "Methods for solving formulas" section below about the differences between algorithms.

One single suitable set of values is enough as a solution: our solver algorithms stop and do not try to find additional solutions. Some of the solver algorithms output the suitable values, but some do not, or output a partial set.

It may also happen that the formula is false for all possible values of variables: if so, the solver algorithms report that after exhausting the search options. For example, (a -> b) & a & -b is always false.

Notice that you can check whether some formula F is always true by trying to solve the negated formula -F: in case -F is always false, F must be always true.

Our solvers may optionally output a trace of the search process. Select "html trace" to see the search process.

For formula-syntax input our solvers first convert the formula to a clause normal form: for certain kinds of formulas this conversion step may create a huge output, but in most cases it is a sensible simplification before actual search.

Methods for solving propositional formulas

There are three main method categories for solving classical propositional formulas:

  • Truth table search: generate all possible assignment combinations for all the variables in the formula and check for each assigment whether the formula is true. Since the number of combinations is two to the power of the number of variables, this becomes infeasible for formulas with a large number of variables.

    This "truth-table: naive" method can be improved by checking also partial assigments where only some variables have been assigned values: it may happen that a formula becomes false even after just a few variables have been assigned. This is implemented as the "truth table: better" method on our page.

  • Resolution search: the idea of the resolution method is to use a gneralization of modus ponens to derive new clauses from the existing clauses. Clauses are derived until all combinations are exchausted or a contradiction is derived. The resolution method should be seen as a general framework: actual solvers implement wildly different strategies and optimisations.

    Our "resolution: naive" method generates clauses in all possible ways and implements no optimizations. The "resolution: better" is significantly optimized: preprocessing clauses, literals in clauses are ordered like [-3-1,2,5], ordered resolution is used (only the first literal of a clause is selected), always selecting the shortest usable clause as given, storing and simplification by unit clauses (assigned variables), forward subsumption of selected clauses and partial backward-subsumption.

    While resolution has been the basis of most state-of-art predicate logic solvers, for propositional logic it is inferior to the DPLL method described next.

  • DPLL (Davis-Putnam-Logemann-Loveland) search is essentially a constraint solver based on the combination of the truth table search with (limited) resolution. For each partial assigment of values in the truth table search we (a) test whether the formula is already false (like the "truth table: better" method above) and (b) use unit clauses (single literals) to derive new unit clauses, which is essentially a limited version of resolution.

    The DPLL method should be also seen as a general framework: actual solvers implement wildly different strategies and optimisations. An excellent source for reading about various methods used by the state of the art solvers is the collection of papers by the authors of Minisat, a popular high-end solver. An important extension to DPLL is Conflict-Driven Clause Learning, currently not implemented by the solvers presented on our page.

    We provide three versions of DPLL solvers for experimenting, from worst (and easiest to understand) to better and more complicated:
    • dpll: naive a minimal, naive implementation of dpll with no optimizations. The code is very similar to the pure table search solver.
    • dpll: old an improved old-style (before the improvements developed in nineties) DPLL. It adds the pure literal rule (used after every unit propagation step), selects literals according to weights calculated before the start of the search, organizes clauses into buckets associated with variables.
    • dpll: better implements additional widely used optimizations on top of the "dpll: old" version (see, for example, minisat papers for explanations):
      • simple preprocessing before search starts: limited unit propagation/subsumption, tautology deletion and pure literal deletion
      • does not use pure literal rule during search (too time-consuming)
      • learning variable weights: the last contradiction clause adds weights to the variables it contains
      • only two literals per clause are watched
      However, the important Conflict-Driven Clause Learning strategy is not implemented.

State of the art propositional solvers

The easiest way to find top level propositional solvers is to check the The international SAT Competition: you will see the competition results for various problem categories, can download competition problems, 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 several other state of the art solvers. You can even run minisat in your browser, compiled from C to javascript using LLVM.

Parsing, converting and printing propositional formulas

The three building options "truth table", "clause normal form" and a "parse tree" are simple, useful utilities implemented in proplog_parse.js and proplog_convert.js:

  • The truth table implemented in proplog_convert.js prints a full truth table of a formula up to 1024 rows: nice for checking out small propositional formulas.

  • The clause normal form implemented in proplog_convert.js is a conjunctive normal form just as used by the solvers. The conversion algorithm used is very simple and does not perform any optimizations. In many cases the optimized converters like the Tseitin transformation would give a much smaller output much faster.

  • The parse tree implemented in proplog_parse.js prints a formula as a nested list built by the simple recursive descent parser. This list is later used by the clause normal form converter to build the form suitable for solvers. Check the parse tree in case you are not sure how the system understands your formula.

Generating propositional problems

Generate a problem button will call generators implemented in proplog_generate.js to generate an example problem in a simple DIMACS format of a clause normal form, suitable for solvers.

The options for the type of a problem are:

  • random 3-sat generates a random set of clauses of length 3, using the number of variables you choose: problems containing more variables are, on the average, harder to solve. The number of clauses is always four times the number of variables: this is, on the average, a specially hard-to-solve ratio for solvers.

    For DPLL try out 200 variables or more. Truth table solvers start running into trouble with more than 20 variables. The resolution provers are a bit better than the truth table solvers, yet much worse than the DPLL solvers.

  • all combinations generates a set of clauses representing all possible combinations of the input variables: any such set is unsatisfiable (i.e. no values of variables can make it true). The number of clauses is hence always two to the power of the number of variables.
  • small unsat generates a very small unsatisfiable clause set, consisting of a single long clause containing all the variables and N single-element clauses containing all variables negated.
The clear button simply clears the input field and result.

You can also browse and read the contents of a file into the input area: essentially copy-paste from a file.