Towards First-order Deduction Based on Shannon Graphs
Joachim Posegga, Bertram Ludäscher
Abstract. We present a new approach to Automated Deduction
based on the concept of Shannon graphs, which are also known as Binary
Decision Diagrams (BDDs). A Skolemized formula is first transformed
into a Shannon graph, then the latter is compiled into a set of Horn
clauses. These can finally be run as a Prolog program trying to refute
the initial formula. It is also possible to precompile axiomatizations
into Prolog and load these theories as required.
[gwai92.ps.gz]