Towards first-order deduction based on Shannon graphs

Joachim Posegga; Bertram Ludäscher

Towards first-order deduction based on Shannon graphs

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English (US)
Title of host publication	GWAI-1992
Subtitle of host publication	Advances in Artificial Intelligence - 16th German Conference on Artificial Intelligence, Proceedings
Editors	Hans Jurgen Ohlbach
Publisher	Springer-Verlag
Pages	67-76
Number of pages	10
ISBN (Print)	9783540566670
State	Published - Jan 1 1993
Externally published	Yes
Event	16th German Workshop on Artificial Intelligence, GWAI 1992 - Bonn, Germany Duration: Aug 31 1992 → Sep 3 1992

Publication series

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

Other

Other	16th German Workshop on Artificial Intelligence, GWAI 1992
Country	Germany
City	Bonn
Period	8/31/92 → 9/3/92

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

Posegga, J., & Ludäscher, B. (1993). Towards first-order deduction based on Shannon graphs. In H. J. Ohlbach (Ed.), GWAI-1992: Advances in Artificial Intelligence - 16th German Conference on Artificial Intelligence, Proceedings (pp. 67-76). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 671 LNAI). Springer-Verlag.

Towards first-order deduction based on Shannon graphs. / Posegga, Joachim; Ludäscher, Bertram.

GWAI-1992: Advances in Artificial Intelligence - 16th German Conference on Artificial Intelligence, Proceedings. ed. / Hans Jurgen Ohlbach . Springer-Verlag, 1993. p. 67-76 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 671 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Posegga, J & Ludäscher, B 1993, Towards first-order deduction based on Shannon graphs. in HJ Ohlbach (ed.), GWAI-1992: Advances in Artificial Intelligence - 16th German Conference on Artificial Intelligence, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 671 LNAI, Springer-Verlag, pp. 67-76, 16th German Workshop on Artificial Intelligence, GWAI 1992, Bonn, Germany, 8/31/92.

Posegga J, Ludäscher B. Towards first-order deduction based on Shannon graphs. In Ohlbach HJ, editor, GWAI-1992: Advances in Artificial Intelligence - 16th German Conference on Artificial Intelligence, Proceedings. Springer-Verlag. 1993. p. 67-76. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Posegga, Joachim ; Ludäscher, Bertram. / Towards first-order deduction based on Shannon graphs. GWAI-1992: Advances in Artificial Intelligence - 16th German Conference on Artificial Intelligence, Proceedings. editor / Hans Jurgen Ohlbach . Springer-Verlag, 1993. pp. 67-76 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{6b115cc6f9814d85b98a3a1cfffcb86a,

title = "Towards first-order deduction based on Shannon graphs",

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.",

author = "Joachim Posegga and Bertram Lud{\"a}scher",

year = "1993",

month = jan,

day = "1",

language = "English (US)",

isbn = "9783540566670",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer-Verlag",

pages = "67--76",

editor = "{Ohlbach }, {Hans Jurgen}",

booktitle = "GWAI-1992",

note = "16th German Workshop on Artificial Intelligence, GWAI 1992 ; Conference date: 31-08-1992 Through 03-09-1992",

}

TY - GEN

T1 - Towards first-order deduction based on Shannon graphs

AU - Posegga, Joachim

AU - Ludäscher, Bertram

PY - 1993/1/1

Y1 - 1993/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0041392545&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0041392545&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0041392545

SN - 9783540566670

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 67

EP - 76

BT - GWAI-1992

A2 - Ohlbach , Hans Jurgen

PB - Springer-Verlag

T2 - 16th German Workshop on Artificial Intelligence, GWAI 1992

Y2 - 31 August 1992 through 3 September 1992

ER -