Towards first-order deduction based on Shannon graphs

Joachim Posegga, Bertram Ludäscher

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationGWAI-1992
Subtitle of host publicationAdvances in Artificial Intelligence - 16th German Conference on Artificial Intelligence, Proceedings
EditorsHans Jurgen Ohlbach
Number of pages10
ISBN (Print)9783540566670
StatePublished - Jan 1 1993
Externally publishedYes
Event16th German Workshop on Artificial Intelligence, GWAI 1992 - Bonn, Germany
Duration: Aug 31 1992Sep 3 1992

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume671 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other16th German Workshop on Artificial Intelligence, GWAI 1992

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Towards first-order deduction based on Shannon graphs'. Together they form a unique fingerprint.

Cite this