Skip to main content
SpringerLink
Log in

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

  • Conference paper
Informatik ’97 Informatik als Innovationsmotor

Part of the book series: Informatik aktuell ((INFORMAT))

  • 176 Accesses

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. T. Arts and J. Giesl. Automatically proving termination where simplification orderings fail. InProc. TAPSOFT’97, vol. 1214 ofLNCS. Springer, 1997.

    Google Scholar 

  2. 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. 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. U. Berger. Program extraction from normalization proofs. InProc. of TLCA’93, Utrecht, 1997.

    Google Scholar 

  5. 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:http://www.uni-koblenz.de/ag-ki/Systems/PROTEIN/.

    Google Scholar 

  6. 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. L. Bachmair, H. Ganzinger, C. Lynch, W. Snyder. Basic Paramodulation.Information and Computation, 121(2):172–192, 1995.

    Article  MathSciNet  MATH  Google Scholar 

  8. 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. 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. 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. 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. F. Baader and K.U. Schulz. Combination Techniques and Decision Problems for Disunification.Theoretical Computer Science B, 142:229-255, 1995.

    Article  MathSciNet  MATH  Google Scholar 

  13. E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACMComputing Surveys, 28(4):626-643, Dec. 1996.

    Article  Google Scholar 

  14. 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. The Economist. Peer review: Shameful, 1997.

    Google Scholar 

  16. 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. J. Guttman, J. Ramsdell, and M. Wand. Vlisp: A verified implementation of SCHEME. Lispand Symbolic Computation, 8: 5–3, 1995.

    Article  Google Scholar 

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

    Article  Google Scholar 

  19. L. Henkin, T. Monk, and A. Tarski.Cylindrical Algebras, Part I. North Holland Publ. Co, 1971.

    Google Scholar 

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

    Chapter  Google Scholar 

  22. 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. W. McCune. Robbins algebras are boolean.Association for Automated Reasoning Newsletter, 35:1–3, 1996.

    Google Scholar 

  24. 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. The Project Mizar. URL:http://www.cs.ualberta.ca/ piotr/Mizar/.

    Google Scholar 

  26. J. Moore. Piton: A verified assembly level language. Technical report 22, Computational Logic Inc., available at the URL: http://www.cli.com, 1988.

    Google Scholar 

  27. L. C. Paulson.Isabelle: A Generic Theorem Prover. Springer, 1994.

    Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

  34. 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. 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. 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. 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. C. Weidenbach. SPASS version0.49. Jour. of Automated Reasoning, 1997.

    Google Scholar 

  39. W. D. Young. A verified code generator for a subset of GYPSY. Technical report, Computational Logic Inc, available at the URL: http://www.cli.co, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. TU Darmstadt, Germany

    Wolfgang Bibel

Authors
  1. Wolfgang Bibel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Lehrstuhl für Informatik V, RWTH Aachen, D-52056, Aachen, Germany

    Matthias Jarke  & Klaus Pohl  & 

  2. Philips GmbH Forschungslaboratorien, Weißhausstr. 2, D-52066, Aachen, Germany

    Klaus Pasedach

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bibel, W. (1997). Deduction as a Cross-Sectional Technology The DFG Focus Programme on Deduction. In: Jarke, M., Pasedach, K., Pohl, K. (eds) Informatik ’97 Informatik als Innovationsmotor. Informatik aktuell. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-60831-5_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-60831-5_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63066-1

  • Online ISBN: 978-3-642-60831-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation