EDBT 2026 Demo / reviewers in the wild / expert
Elmar Eder
dblp:40/3840
· DBLP profile ↗
4ranked-venue papers
2as first author
0since 2021 · last 1997
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Artificial intelligence and machine learning · 2 · 1 first-authorGraphics, computer vision, multimedia, augmented reality and games · 2 · 1 first-authorTheory of computation · 1 · 1 first-authorApplied, interdisciplinary, general and emerging computing · 1
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Theoretical computer science
3 papers |
Logic in computer science · 44% Automated reasoning and model checking · 31% Computational complexity · 26% |
Topics — the 5 heaviest of 5, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Automated reasoning and model checking
theorem proving |
0.0 | 3 | 1997 | Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution · J. ACM 1997 Consolution and its Relation with Resolution · IJCAI 1991 Towards an Advanced Implementation of the Connection Method · IJCAI 1983 |
Logic in computer science
proof theory |
0.0 | 2 | 1997 | Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution · J. ACM 1997 Consolution and its Relation with Resolution · IJCAI 1991 |
Computational complexity › proof complexity
resolution |
0.0 | 2 | 1997 | Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution · J. ACM 1997 Consolution and its Relation with Resolution · IJCAI 1991 |
Logic in computer science
completeness |
0.0 | 1 | 1997 | Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution · J. ACM 1997 |
Automated reasoning and model checking › automated theorem proving
connection method |
0.0 | 1 | 1983 | Towards an Advanced Implementation of the Connection Method · IJCAI 1983 |
Methods — techniques the papers use, named apart from their topics
resolution · 0.0decomposition · 0.0unification · 0.0connection method · 0.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 1997 | Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolutionabstractThis paper addresses and answers a fundamental question about resolution. Informally, what is gained with respect to the search for a proof by performing a single resolution step? It is first shown that any unsatisfiable formula may be decomposed into regular formulas provable in linear time (by resolution). A relevant resolution step strictly reduces at least one of the formulas in the decomposition while an irrelevant one does not contribute to the proof in any way. the relevance of this insight into the nature of resolution and of the unsatisfiability problem for the development of proof strategies and for complexity considerations are briefly discussed. The decomposition also provides a technique for establishing completeness proofs for refinements of resolution. As a first application, connection-graph resolution is shown to be strongly complete. This settles a problem that remained open for two decades despite many proff attempts. The result is relevant for theorem proving because without strong completeness a connection graph resolution prover might run into an infinite loop even on the ground level. Wolfgang Bibel, Elmar Eder |
J. ACM | 2 |
| 1991 | Consolution and its Relation with Resolution
Elmar Eder |
IJCAI | 1 |
| 1985 | Properties of Substitutions and Unifications
Elmar Eder |
J. Symb. Comput. | 1 |
| 1983 | Towards an Advanced Implementation of the Connection Method
Wolfgang Bibel, Elmar Eder, Bertram Fronhöfer |
IJCAI | 2 |