Cannot detect infinite trees

[ixjf]

Since the algorithm doesn't foresee any patterns and always follows the same rules in the same order, some inputs may lead to trees that become stuck in an infinite EQ->UQ cycle. No clue how to solve. Haven't given it much thought yet. I mean, if it ends up in an infinite cycle, then the tree is open. The problem is: how do I know if I'm in an infinite loop?

Specific instances where it fails:

(∀x)(L¹x ⊃ (∃y)(F¹y & (∃z)(T¹z & P³xyz))),
(∃x)(L¹x)
∴ (∃x)(F¹x & (∃y)(T¹y & (∃z)(L¹z & P³zxy)))

{∀x((A¹x & B¹x) ⊃ ∀y(~C¹y ⊃ ∃z(A²zy & B¹z)))}

∀x(S¹x ⊃ (∃y)(F¹y & M²xy)),
F¹b
∴ ∃x(S¹x & H²bx)

∃x(C¹x & ~(∃y)(G¹y & E²xy))

[ixjf]

http://www.cogsci.rpi.edu/~heuveb/teaching/Logic/CompLogic/Web/Handouts/FO-Completeness-Truth-Tree.pdf

Following this, I can guarantee that if the algorithm generates an infinite tree, then the initial set of statements is satisfiable. I.e. there's no way for the algorithm to generate an infinite truth tree from a set of statements that is unsatisfiable, which is a start.

All examples are satisfiable, and they do lead to an infinite tree.

A solution to knowing whether the algorithm is stuck in an infinite loop is to simply limit the number of possible constants. That, obviously, means not strictly following the book, and also leads to huge trees. Preferably, we would find some way to detect a long-running algorithm and stop, but that's also unreliable. Unfortunately, first-order logic is undecidable, so whatever we do, it'll never work 100%.

[ixjf]

A possibility to work around infinite trees is providing an option to stop the algorithm as soon as it is clear that a set of statements is satisfiable (i.e. as soon as one branch is open). There will still be cases where this won't work (where all branches have an infinite number of statements), but it should solve the majority of cases (I guess). However, it still leaves a tree with potentially unfinished branches.

[ixjf]

A better idea is to implement a callback on every iteration of the loop of the truth tree algorithm so that a human can check the progress in real time and catch infinite trees. A person could easily tell in most cases. This wouldn't require limiting the language at all. The call back could ask for a Boolean return value, as in whether it should continue or stop. The website would run the truth tree algorithm in a separate thread as to not freeze the website. The website would give the option of continuing/pausing/stopping, plus variable delay between iteration. After clicking "Stop", you'd press "Validate" to have the truth tree analysed.

[ixjf]

The idea just above would put some burden on the user to verify the validity of the result. An alternative, which still has this issue to but to a lesser extent, would be to implement some sort of algorithm to look for repeating patterns in a branch. This wouldn't be able to give accurate results 100% of the time, but probably would give the correct result most of the time.