Description: Online logic solvers.
logic (490) resolution (232) reasoning (61) propositions (14) solvers (3) dpll (3) truth table (2)
Result: Hide help What is this? A toolkit for proving first order predicate 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 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 th
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 an
We will give two facts: john is a father of pete and pete is a father of mark . We will ask whether from these two facts we can derive that john is a father of pete : obviously we can.