Deduction as a Cross-Sectional Technology The DFG Focus Programme on Deduction

  • Wolfgang Bibel
Conference paper
Part of the Informatik aktuell book series (INFORMAT)


This paper outlines the major research issues pursued in the DFG Focus Programme on Deduction, highlights some of the results achieved and points out the relevance of deduction as a cross-sectional technology1.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AG97]
    T. Arts and J. Giesl. Automatically proving termination where simplification orderings fail. InProc. TAPSOFT’97, vol. 1214 ofLNCS. Springer, 1997.Google Scholar
  2. [BBER94a]
    W. Bibel, S. Brüning, U. Egly, and T. Rath. KoMeT. In A. Bundy, editor,Proc. of the Int. Conference on Automated Deduction, CADE-12, vol. 814 of LNAI, pages 783–787, Springer, 1994.Google Scholar
  3. [BBER94b]
    W. Bibel, S. Brüning, U. Egly, and T. Rath. Towards an adequate Theorem Prover Based on the Connection Method. In I. Plander, editor,Proc. of the 6th Int. Conference on Artificial Intelligence and Information-Control of Robots, pages 137–148. World Scientific Publishing Company, 1994.Google Scholar
  4. [Ber97]
    U. Berger. Program extraction from normalization proofs. InProc. of TLCA’93, Utrecht, 1997. Google Scholar
  5. [BF94]
    P. Baumgartner and U. Furbach. PROTEIN: APROver with a Theory Extension Interface. In A. Bundy, editor,Proc. of the Int. Conference on Automated Deduction, LADE-1,2, vol. 814 of LNAI, pages769-773, Springer, 1994. Available in the WWW, URL: Scholar
  6. [BGK96]
    R. Bündgen, M. Göbel, and W. Küchlin. Strategy compliant multithreaded term completion. Journal of Symbolic Computation, 21(4–6):475–505, 1996.Google Scholar
  7. [BGLS95]
    L. Bachmair, H. Ganzinger, C. Lynch, W. Snyder. Basic Paramodulation.Information and Computation, 121(2):172–192, 1995.MathSciNetzbMATHCrossRefGoogle Scholar
  8. [BHK95]
    A. Beringer, S. Hölldobler, and F. Kurfeß. Spatial Reasoning and Connectionist Inference. In R. Bajcsy, editor,Proc. of the Int. Joint Conference on Artificial Intelligence, IJAI-95, pages1352–1357. IJCAII, Morgan Kaufmann, San Mateo, 1995.Google Scholar
  9. [BHOS96]
    B. Beckert, R. Höhnle, P. Oel, and M. Sulzmann. The tableau-based theorem prover 3TAP, version 4.0. In M. McRobbie and J. Slaney, editors,Proc. of the Int. Conference on Automated Deduction, LADE-13, vol. 1104, pages303–307, 1996.Google Scholar
  10. [BKKS96]
    W. Bibel, D. Korn, C. Kreitz, and S. Schmitt. Problem-oriented applications of automated theorem proving. In L. Carlucci Aiello, editor,Proc. of the Int. Symposium on Design and Implementation of Symbolic Computation Systems (DISCO’96), vol. 1128 of LNCS, pages 1–21, Springer, 1996.Google Scholar
  11. [BR95]
    E. Börger and D. Rosenzweig. The WAM-definition and compiler correctness. In C. Beierle and L. Plümer, editors,Logic Programming: Formal Methods and Practical Applications, vol. 11 of Studies in Computer Science and Artificial Intelligence, Amsterdam, 1995. North-Holland.Google Scholar
  12. [BS95]
    F. Baader and K.U. Schulz. Combination Techniques and Decision Problems for Disunification.Theoretical Computer Science B, 142:229-255, 1995.MathSciNetzbMATHCrossRefGoogle Scholar
  13. [CW96]
    E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACMComputing Surveys, 28(4):626-643, Dec. 1996.CrossRefGoogle Scholar
  14. [DFF97]
    J. Denzinger, Marc Fuchs, and Matthias Fuchs. High performance ATP systems by combination of several AI methods. InProc. of IJCAI’97, to appear, 1997.Google Scholar
  15. [Eco97]
    The Economist. Peer review: Shameful, 1997.Google Scholar
  16. [FKS95]
    B. Fischer, M. Kievernagel, and G. Snelting. Deduction-based software component retrieval. InProc. IJCAI-95 Workshop on Formal Approaches to the Reuse of Plans, Proofs, and Programs, August 1995.Google Scholar
  17. [GRW95]
    J. Guttman, J. Ramsdell, and M. Wand. Vlisp: A verified implementation of SCHEME. Lispand Symbolic Computation, 8: 5–3, 1995.CrossRefGoogle Scholar
  18. [HKK+96]
    X. Huang, M. Kerber, M. Kohlhase, E. Melis, D. Nesmith, J. Richts, and J. Siekmann. Die Beweisentwicklungsumgebung ?-MKRP.Informatik - Forschung and Entwicklung, 11(1):20–26, 1996. in German.CrossRefGoogle Scholar
  19. [HMT71]
    L. Henkin, T. Monk, and A. Tarski.Cylindrical Algebras, Part I. North Holland Publ. Co, 1971.Google Scholar
  20. [Hod95]
    I. Hodkinson. Expressive Completeness of UNTIL and SINCE over Dedekind Complete Linear Time. InModal Logic and Process Algebra. A Bisimulation Perspective, pages 171–185. SCLI Publications, 1995.Google Scholar
  21. [IL97]
    O. Ibens and R. Letz. Subgoal Alternation in Model Elimination. In D. Galmiche, editor,Automated Reasoning with Analytic Tableaux and Related Methods, vol. 1227 of LNAI, pages 201–215, 1997. CrossRefGoogle Scholar
  22. [KW95]
    T. Kolbe and C. Walther. Second-order matching modulo evaluation — a technique for reusing proofs. InProc. of the 11th Int. Joint Conference on Artificial Intelligence, Montreal, Canada, 1995.Google Scholar
  23. [McC96]
    W. McCune. Robbins algebras are boolean.Association for Automated Reasoning Newsletter, 35:1–3, 1996.Google Scholar
  24. [MIL+97]
    M. Moser, 0. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, and K. Mayr. SETHEO and E-SETHEO.Jour. of Automated Reasoning, 1997. Google Scholar
  25. [Miz]
    The Project Mizar. URL: piotr/Mizar/.Google Scholar
  26. [Moo88]
    J. Moore. Piton: A verified assembly level language. Technical report 22, Computational Logic Inc., available at the URL:, 1988.Google Scholar
  27. [Pau94]
    L. C. Paulson.Isabelle: A Generic Theorem Prover. Springer, 1994.Google Scholar
  28. [Pus96]
    C. Pusch. Verification of compiler correctness for the WAM. InProc. of the 1996 Int. Conference on Theorem Proving in Higher Order Logics, LNCS. Springer, 1996.Google Scholar
  29. [Rei95]
    W. Reif. The KIV-approach to software verification. In M. Broy and S. Jahnichen, editors,KORSO: Methods, Languages, and Tools for the Construction of Correct Software - Final Report, vol. 1009 ofLNCS. Springer, 1995.Google Scholar
  30. [RS93]
    W. Reif and K. Stenzel. Reuse of proofs in software verification. In R. Shyamasundar, editor,Foundation of Software Technology and Theoretical Computer Science. Proceedings, vol. 761 of LNCS. Springer, 1993.Google Scholar
  31. [RSS19]
    W. Reif, G. Schellhorn, and K. Stenzel. Proving system correctness with KIV 3.0. In Proc. ofthe Int. Conference on Automated Deduction, CADE14, to appear. Springer, 1997.Google Scholar
  32. [RSS95]
    W. Reif, G. Schellhorn, and K. Stenzel. Interactive correctness proofs for software modules using kiv. InTenth Annual Conference on Computer Assurance, Gaithersburg (MD), USA, 1995. IEEE press.Google Scholar
  33. [SA97]
    G. Schellhorn and W. Ahrendt. Reasoning about Abstract State Machines: The WAM Case Study.Jour. of Universal Computer Science (JUCS), 3 (4): 377–413, 1997.MathSciNetzbMATHGoogle Scholar
  34. [Sch95]
    A. Schönegge. Extending dynamic logic for reasoning about evolving algebras. Technical Report 49/95, Fakultät für Informatik, Universität Karlsruhe, 76128 Karlsruhe, Germany, 1995.Google Scholar
  35. [SSY94]
    G. Sutcliffe, C.B. Suttner, and T. Yemenis. The TPTP problem library. In A. Bundy, editor, Proc. ofthe Int. Conference on Automated Deduction, LADE-91, vol. 814 of LNAI, pages252–266. Springer, 1994.Google Scholar
  36. [ST96]
    F. Stolzenburg and B. Thomas. Analysing rule sets for the calculationofbanking fees by a theorem prover with constraints. In Proc. of the 2nd Int. Conference on Practical Application of Constraint Technology, pages269-282, London, April1996. Practical Application Company.Google Scholar
  37. [vHLS97]
    F.W. von Henke, M. Luther, and M. Strecker. TYPELAB: An environment for modular program development. In M. Dauchet, M. Bidoit, editors,Proc. of TAPSOFT’97, vol. 1214 of LNCS, pages851–854. Springer, 1997.Google Scholar
  38. [Wei97]
    C. Weidenbach. SPASS version0.49. Jour. of Automated Reasoning, 1997. Google Scholar
  39. [You88]
    W. D. Young. A verified code generator for a subset of GYPSY. Technical report, Computational Logic Inc, available at the URL:, 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Wolfgang Bibel
    • 1
  1. 1.TU DarmstadtGermany

Personalised recommendations