Compiling Proof Search in Semantic Tableaux

An approach to implementing deduction systems based on semantic tableaux is described; it works by compiling a graphical representation of a fully expanded tableaux into a program that performs the search for a proof at runtime. This results in more efficient proof search, since the tableau needs not to be expanded any more, but the proof consists of determining whether it can be closed, only. It is shown how the method can be applied for compiling to the target language Prolog, although any other general purpose language can be used.

• Type: Conference
• Year: 1993
• Where: ISMIS
• Authors: Joachim Posegga
• Keywords: Artificial Intelligence, Efficient Proof Search, ISMIS 1993, Semantic Tableaux, Target Language Prolog