logic-rs

logic-rs is a parser of relational predicate logic and truth tree solver written in Rust. This page provides the frontend to it.
Being heavily influenced by the book Meaning and Argument: An Introduction To Logic Through Language, by Ernest Lepore and Sam Cumming, and trying to follow as closely as possible its grammar and rules, it:

provides syntax to distinguish between statement sets, arguments, and single statements as input
produces detailed truth trees
analyses the truth trees to auto-check the consistency of statement sets, the formal validity of arguments, and the logical properties of statements, namely contradiction, tautology, and contingency.

You're welcome to view and contribute to the project on GitHub. Both the website and library are hosted there.

In the editor above, you can type in either a statement set, an argument, or a single statement, following the grammar as specified below.

If you'd like to have a look at a more detailed specification of the language, you can browse to the wiki on the GitHub repository by clicking here.

Once you're finished, click "Solve" at the top of the editor. One or more detailed truth trees should appear, along with the result of the analysis of the truth trees. If the truth trees are too large, you can zoom in and out with either mouse or touch, as well as move them around with mouse, touch, or keyboard.

In order to type in the Unicode tokens, either use the buttons on the toolbar, or use the available keyboard shortcuts if on PC. You can find the keyboard shortcut for each token by hovering over each button on the toolbar.

White spaces are allowed anywhere except in between component tokens of terms and component tokens of atomic formulas, namely singular statements, simple predicates with terms attached, and simple statements.

Syntax	Meaning
<formula>	Groupers. They specify precendence over connectives. They are mandatory in certain cases, like around conjunction, disjunction, and conditional formulas.
<statement-list>	Statement set. The inner expression is one or more statements separated by a comma.
<statement-list> <statement>	Argument. 'statement-list' is one or more statements separated by a comma (but without a comma before the conclusion indicator), and 'statement' is a single statement.
A_p	Simple statement. 'A' is any character from 'A' to 'Z', and 'p' any positive integer. 'p' must be in Unicode subscript and cannot have leading zeros. A simple statement is a formula.
<formula> <formula>	Conjunction of formulas. If both formulas are statements, the resulting expression is a complex statement. If both formulas are predicates, the resulting expression is a compound predicate. In either case, the resulting expression is a formula.
<formula>	Negation of a formula. If the formula is a statement, the resulting expression is a complex statement. If the formula is a predicate, the resulting expression is a compound predicate. In either case, the resulting expression is a formula.
<formula> <formula>	Disjunction of formulas. If both formulas are statements, the resulting expression is a complex statement. If both formulas are predicates, the resulting expression is a compound predicate. In either case, the resulting expression is a formula.
<formula> <formula>	Conditional formula. If both formulas are statements, the resulting expression is a complex statement. If both formulas are predicates, the resulting expression is a compound predicate. In either case, the resulting expression is a formula.
a_p	Singular term. 'a' is any character ranging from 'a' to 'w', and 'p' is any positive integer in Unicode subscript without leading zeros.
A_p^qa₀a₁..a_n	Simple predicate/singular statement, where 'A' is any character from 'A' to 'Z', 'p' is any number in Unicode subscript without leading zeros, 'q' is any positive integer in Unicode superscript without leading zeros ('q' represents the degree of the predicate, i.e. the number of terms attached), and 'a₀a₁..a_n' is one or more terms (singular terms & variables) attached to this predicate. If all terms are singular terms, then this is a singular statement, not a simple predicate.
x<formula> x<formula>	Existential statement. 'x' is any variable.
x<formula> x<formula>	Universal statement. 'x' is any variable.
x₀	Variable. 'x' is any character from 'x' to 'z', and '0' any positive integer in Unicode subscript without leading zeros.

About

Usage