KromHornSolver

The KromHornSolver generates the evolution of a Splitting Turing Machine (STM), the corresponding tableau in the tableaux calculus and the corresponding proof search in the NNF-calculus up to an upper bound.
The evolutions are printed by color diagrams.
For details cf. Lampert / Nakano, Explaining Undecidability of First-Order Logic, detailed output of STM1 described in the paper and detailed output of STM2 described in the paper. Cf. also software on github.

STM1/2 from the below menu are not identical with STM1/2 described in the above paper.
Rather, STM9/M10 from the below menu are identical to STM1/2 of the paper despite that they start with a simplified input on the tape.
STM9 halts with upper bound 174, STM10 does not halt. Yet, their evolution diagrams for the first 43 (STM) / 173 (proofs) steps do not differ.

Either select an STM :

Or enter an STM by hand:

{{P, H}, {0, 1}, {{P, 0, {R}, P}, {P, 1, {R}, H}}, P, H, {0, 0, 1}}

Enter an upper bound for the tableaux proof search (a number between 1 and 320, the lower you choose the smaller the diagram will be printed):

Enter a time constraint in seconds up to 300:

The evolution diagram of the STM:

The evolution diagram of the mainbranch in the tableau up to the upperbound:

The evolution diagram of the NNF-C. proof search up to the upperbound (each splitting expression + rest separated by white line):

Datenschutzerklaerung

© Timm Lampert / 2022-05-05