T* SCI

You can input your formula using the following convention:

```
=
```
for identity
```
->
```
for implication
```
-
```
for negation
```
&
```
for conjunction
```
|
```
for alternative
```
<>
```
for equivalence
and a string of alpha-numeric characters for the variables (e.g.
```
p
```
,
```
phi
```
,
```
v1
```
,
```
ϕ
```
)

You can input multiple formulas, separated by "

".
You will get a proof tree. The proof tree is an attempt at proving that the provided formulas, as a conjunction, are necessarily false. For example a proof tree:

--: {¬¬(p≡q)}	(is open) applied rule ¬ to ¬¬(p≡q)
  |--: {(p≡q)}	(is open) applied rule ≡⊤ to (p≡q)
  | |--: {p, q, (p≡q)}	(is open)
  | |--: {¬p, ¬q, (p≡q)}	(is ?)

Means that:

your formula is
```
¬¬(p≡q)
```
,
rule
```
¬
```
applies to it and it produces formula
```
(p≡q)
```
,
to which rule
```
≡⊤
```
applies. It produces two sub-branches:
```
p, q, (p≡q)
```
and
```
¬p, ¬q, (p≡q)
```
.
To the branch
```
p, q, (p≡q)
```
no further rules apply and it is not an axiom-branch (i.e. it is not trivially false) which means that this branch can be true. It is marked by stating that this branch is open.
If any of the sub-branches is open, the further branches (if any) are not calculated and no rules are applied to them. They are marked as "?".
If the branch is trivially false or all its sub-branches are closed, the branch is marked as closed.

A couple of notes:

This implementation doesn't use the rule
```
sym
```
. Instead, every formula, after its parsing or creation is "normalized", which means that the left side of "=" is "smaller" than the right side.
Sets of rules are similarly ordered and normalized (e.g. if a rule would produce
```
{p, -p, p, p}
```
, it will produce
```
{p, -p}
```
instead). In a similar way, the sub-branches are sorted and repeating ones are eliminated.
The performance could be improved. If you see no output for a long time, the formula you provided is too complex. Let me know and I'll improve the performance.
The source code can be found at https://github.com/AdrianSiwiec/sci

Changelog:

07.04.2024 - Fixes:
- fixed bug in
```
fun
```
  rule implementation
- single-use rules are now single-use in a branch not globally
- input can contain utf-8 symbols of
```
≡, ¬, →, ↔, ∧, ∨
```
  (to ease copy-pasting output)
- major performance improvements.
25.04.2024 - Fixed two bugs that were causing the results to be incorrectly "open" in some cases. The fix changes the order of applied rules in some cases, unfortunately making formula
```
-ψ
```
too difficult for the current implementation.
06.05.2024 - Fixed sym rule. Previously some formulas were incorrectly deemed to be closed.

NOTE: to see the improvements you might need to hard-refresh this page (ctrl+shift+r) to reload the binary. Otherwise you might be using the old binary (it won't work for ϕ and -ϕ below)

Click to see a labelled Tableau implementation -- a different algorithm solving the exact same problem.

You can click on the following examples to see their proof trees, or input your own formulas below.

(Example from Table 7 from the T* paper.)
(Formula ϕ from "Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity")
(Formula -ϕ from ibid.)
(Formula ψ, equal to φ(p/φ) from ibid.)

T* algorithm implementation