Towards first-order deduction based on Shannon graphs

Joachim Posegga; Bertram Ludäscher

doi:10.1007/bfb0018993

Towards first-order deduction based on Shannon graphs

Joachim Posegga
, Bertram Ludäscher

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
Pages	67-76
Number of pages	10
ISBN (Print)	9783540566670
DOIs	https://doi.org/10.1007/bfb0018993
State	Published - 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/Territory	Germany
City	Bonn
Period	8/31/92 → 9/3/92

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/bfb0018993

Library availability

Discover UIUC Full Text

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. https://doi.org/10.1007/bfb0018993

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, 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, pp. 67-76, 16th German Workshop on Artificial Intelligence, GWAI 1992, Bonn, Germany, 8/31/92. https://doi.org/10.1007/bfb0018993

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. 1993. p. 67-76. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/bfb0018993

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

doi = "10.1007/bfb0018993",

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

pages = "67--76",

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

booktitle = "GWAI-1992",

address = "Germany",

}

TY - GEN

T1 - Towards first-order deduction based on Shannon graphs

AU - Posegga, Joachim

AU - Ludäscher, Bertram

PY - 1993

Y1 - 1993

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 - https://www.scopus.com/pages/publications/0041392545

UR - https://www.scopus.com/pages/publications/0041392545#tab=citedBy

U2 - 10.1007/bfb0018993

DO - 10.1007/bfb0018993

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

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

Y2 - 31 August 1992 through 3 September 1992

ER -

Towards first-order deduction based on Shannon graphs

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this