On: LangPro: Natural Language Theorem Prover

[nurettin]

I mean how does the pruning constraint tree search applied in prolog implementations differ from the tableaux method

[nurettin → nurettin]

After some research, the tableaux method seems to require full coverage, which would only converge with the search tree if all conditions have to be exhausted.