Bibel, Wolfgang

Interpretation of published papers

Code, NrCitation
1   
address
Wolfgang Bibel's Home Page

Dr. Wolfgang Bibel, Professor

Address

FG Intellektik, FB Informatik
Technische Hochschule Darmstadt
Alexanderstr. 10,
D-64283 Darmstadt
Germany

Email: bibel@intellektik.informatik.th-darmstadt.de
Phone: ++ 49 (0) 6151 16 2100
Fax: ++ 49 (0) 6151 16 5326

Office: Alexanderstr. 10, Room 107


2   
#resume
3   
NIL

Résumé


Wolfgang Bibel is Professor for Intellectics at the Department of Computer Science of the Darmstadt Institute of Technology in Germany. He also maintains an affiliation with the University of British Columbia as Adjunct Professor. In 1968 he received a Ph.D. degree from the Ludwig-Maximilian University of Munich, Germany. For many years he worked at the Technical University of Munich as a Senior Researcher, building up the AI group there. In 1987 he became a Professor in Computer Science at the University of British Columbia, Vancouver, and a Fellow of the Canadian Institute for Advanced Research. His more than one hundred and fifty publications range over various areas in artificial intelligence such as automated deduction, machine architecture for deductive systems, program synthesis, knowledge representation, and include also topics concerning the implications of AI technology for society. Dr. Bibel is Section Editor of the Artificial Intelligence Journal, Associate Editor of the Journal for Symbolic Computation, Co-Editor of the AI book series of Vieweg Verlag, and on the board of seven more journals. From 1982 through 1986 he served as the first Chairman of ECCAI, the European AI organization. From 1987 through 1995 he was a Trustee of the International Joint Conferences for Artificial Intelligence, Inc., and held the Conference Chair of IJCAI'89. Currently he is coordinating a national six year research programme on deduction. In 1990 he has been awarded the title of an {\em AAAI Fellow\/} by the American Association for Artificial Intelligence (AAAI) ``in Recognition of Significant Contributions to the Field of Artificial Intelligence''. In 1996 he received the German research excellence award for Artificial Intelligence from the Association of German AI Institutions (AKI). Currently, Dr. Bibel is the conference chair of the 15th International Conference on Automated Deduction (CADE-15) taking place 5-10 July 1998 in Lindau, Germany, at the beautiful Lake Constance.

4   
NIL

Group activities

  • Deduction
    Deduction is a central mechanism on which many AI activities are based. The connection method provides the logical basis for automated theorem proving carried out in our group. Several theorem provers for first-order predicate logic have been developed. Thereby we aim at integrating as many special techniques as possible within the general framework of the connection method. Machine-oriented connection proofs are transformed into a form appropriate for human understanding.
  • Knowledge Representation
    Knowledge is an essential part for achieving intelligent behavior. We are committed to a logical form of representing knowledge since this allows the import of great reasoning power from deduction. Over the time many aspects of reasoning have been studied by members of the group such as non-monotonicity, modalities, fuzziness and so forth.
  • Program Synthesis
    The automation of software production by way of synthesis from declarative specifications is considered one of the most problems for Artificial Intelligence. In the recent years we have pursued the proofs-as-programs paradigm in constructive logics. This led to the development theorem provers for intuitionistic logic on the basis of those developed for classical logic so that all features from those could be imported. The work is pursued in the framework of the NuPRL verified program development system.
  • Logic Programming
    Equational theories are of importance in many areas of computer science and AI. To incorporate such theories into a deductive mechanism like the one used in logic programming, enhanced unification algorithms are studied and extensions of the standard resolution strategies (which on Horn clauses are identical with connection method strategies) are explored.
  • Reasoning about Actions
    To solve the classical AI planning problem several approaches based on the resource paradigm have been developed and are still being explored. In particular, we were able to solve the frame problem this way. On this basis we investigate ontological extensions such as non-deterministic and concurrent actions, the ramification problem, and hierarchical planning. Furthermore, we have explored, extended and compared high-level specification languages such as A (Gelfond and Lifschitz) and the Ego-World-Semantics (Sandewall).
    An assistance planning system has been designed and is used to develop and verify interactive planning methods to support a human user.
  • Connectionistic Systems
    Connectionism bases on the idea of parallel distributed processing. On the model of the human brain, artificial neural networks break up complex tasks into numerous parallel subtasks. Our group has been interested especially to model reasoning in such systems in order to get some understanding how reasoning might be realized in the brain.
  • Stochastic Search
    Stochastic Search methods can be used to solve hard combinatorial optimization problems efficiently. In this field we work with stochastic search methods for the solution of satisfiability problems (SAT) and Constraint Satisfaction Problems. We aim to develop massively parallel search methods, based on neural networks, for the solution of SAT. Search methods inherent in natural systems are studied for the solution of hard combinatorial optimization problems. Here our research focuses on ant colony optimization, an approach which models the behavior of ant colonies and is used to solve function or combinatorial optimization problems.

5   
NIL

Selected Publications



    1997


6   
publications/aij97.ps.gz
  • Wolfgang Bibel:
    Let's Plan It Deductively (Invited Paper). 15th International Joint Conference on Artificial Intelligence (IJCAI-97) , August 23-29, Nagoya, Japan. pp. 1549-1562
    bib-tex (abstract) (gzipped postscript file, 96k)

    • 7   
    NIL
  • Wolfgang Bibel and Elmar Eder:
    Decomposition of Tautologies into Regular Formulas and Strong Completeness of Connection-Graph Resolution. Journal of the ACM 44(2) , pp. 320-344
    bib-tex


    • 8   
    NIL
  • Wolfgang Bibel and Daniel Korn and Christoph Kreitz and F Kurucz and Jens Otten and Stephan Schmitt and Gerd Stolpmann:
    A Multi-level Approach to Program Synthesis. Proceedings of the 7th Workshop on Logic Program Synthesis and Transformation (LOPSTR-97) , LNCS, Springer Verlag, Berlin.
    bib-tex (gzipped postscript file, 155k)

    • 9   
    NIL

    1996


    10   
    NIL
  • Wolfgang Bibel and Michael Thielscher:
    Non-Classical Automated Deduction. In: Trends in Theoretical Informatics (R. Albrecht, H. Herre, Eds.) , Oldenbourg, Wien, 39-59.

    • 11   
    NIL
  • Wolfgang Bibel, Daniel Korn, Christoph Kreitz, and Stephan Schmitt:
    Problem-Oriented Applications of Automated Theorem Proving. Proceedings of the International Symposium on Design and Implementation of Symbolic Computation Systems (DISCO'96), (L. Carlucci Aiello, Ed.) , LNCS 1128, Springer, Berlin, 1-21.


    • 12   
    NIL

    1995


    13   
    NIL
  • Wolfgang Bibel, Stefan Brüning, Uwe Egly, Daniel Korn, and Thomas Rath:
    Issues in Theorem Proving Based on the Connection Method. Theorem Proving with Analytical Tableaux and Related Methods, Proceedings of the Fourth International Workshop, TABLEAUX'95, (P. Baumgartner, R. Hähnle, J. Posegga, Eds.) , LNAI 918, Springer, Berlin, 1--16.

    • 14   
    NIL

    earlier


    15   
    NIL
  • Wolfgang Bibel, Stefan Brüning, Uwe Egly, and Thomas Rath:
    KoMeT. In CADE-94 (A. Bundy, Ed.), LNAI, Springer, Berlin, 783--787, 1994.

    • 16   
    NIL
  • Wolfgang Bibel and Elmar Eder:
    Methods and Calculi for Deduction. Chapter 3 in: Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 1 (D.M. Gabbay, C.J. Hogger, J.A. Robinson, Eds) , Oxford University Press, 67--182, 1993.

    • 17   
    NIL
  • Wolfgang Bibel:
    Deduction: Automated Logic. Academic Press, London, 242 pp, 1993.

    • 18   
    NIL
  • Wolfgang Bibel and R. Letz and J. Schumann and S. Bayerl:
    SETHEO: A High-Performance Theorem Prover. Journal of Symbolic Computation 15(5-6) , pp. 183-212, 1992.

    • 19   
    NIL
  • Wolfgang Bibel:
    Perspectives on Automated Deduction. In: Automated Reasoning: Essays in Honor of Woody Bledsoe (R.S. Boyer, Ed.) , Kluwer Academic Publishers, Utrecht, 77-104, 1991.

    • 20   
    NIL
  • Wolfgang Bibel:
    Short Proofs of the Pigeonhole Formulas Based on the Connection Method. Journal of Automated Reasoning 6 , pp. 287-297, 1990.

    • 21   
    NIL
  • Wolfgang Bibel:
    A Deductive Solution for Plan Generation. New Generation Computing 4 , pp. 115--132, 1986.

    • 22   
    NIL
  • W. Bibel and B. Buchberger:
    Towards a Connection Machine for Logical Inference. Future Generations Computer Systems Journal 1 , pp. 177-188, 1985.

    • 23   
    NIL
  • Wolfgang Bibel:
    Automated Inferencing. Journal of Symbolic Computation 1 , pp. 245--260, 1985.

    • 24   
    NIL
  • Wolfgang Bibel:
    Automated Theorem Proving. Vieweg Verlag, Wiesbaden, 293 pp. (1982); 2. Edition 289 pp, 1987.



    Current Projects:

    • 25   
    NIL
  • SALIERI (Computer music)
    Currently supported by the Computer Science Department and the Center for Interdisciplinary Technical Studies (ZIT) of the Darmstadt University of Technology
    Participants:
    • 26   
    NIL

    Courses:
    Generated by Christoph Herrmann (chris@informatik.th-darmstadt.de) and
    Michael Thielscher (mit@informatik.th-darmstadt.de)

    Mainained by Thomas Stützle (stuetzle@informatik.th-darmstadt.de) and
    Hartmut Bittner (bittner@informatik.th-darmstadt.de)