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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
T. Arts and J. Giesl. Automatically proving termination where simplification orderings fail. InProc. TAPSOFT’97, vol. 1214 ofLNCS. Springer, 1997.
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.
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.
U. Berger. Program extraction from normalization proofs. InProc. of TLCA’93, Utrecht, 1997.
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/.
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.
L. Bachmair, H. Ganzinger, C. Lynch, W. Snyder. Basic Paramodulation.Information and Computation, 121(2):172–192, 1995.
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.
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.
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.
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.
F. Baader and K.U. Schulz. Combination Techniques and Decision Problems for Disunification.Theoretical Computer Science B, 142:229-255, 1995.
E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACMComputing Surveys, 28(4):626-643, Dec. 1996.
J. Denzinger, Marc Fuchs, and Matthias Fuchs. High performance ATP systems by combination of several AI methods. InProc. of IJCAI’97, to appear, 1997.
The Economist. Peer review: Shameful, 1997.
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.
J. Guttman, J. Ramsdell, and M. Wand. Vlisp: A verified implementation of SCHEME. Lispand Symbolic Computation, 8: 5–3, 1995.
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.
L. Henkin, T. Monk, and A. Tarski.Cylindrical Algebras, Part I. North Holland Publ. Co, 1971.
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.
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.
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.
W. McCune. Robbins algebras are boolean.Association for Automated Reasoning Newsletter, 35:1–3, 1996.
M. Moser, 0. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, and K. Mayr. SETHEO and E-SETHEO.Jour. of Automated Reasoning, 1997.
The Project Mizar. URL:http://www.cs.ualberta.ca/ piotr/Mizar/.
J. Moore. Piton: A verified assembly level language. Technical report 22, Computational Logic Inc., available at the URL: http://www.cli.com, 1988.
L. C. Paulson.Isabelle: A Generic Theorem Prover. Springer, 1994.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
C. Weidenbach. SPASS version0.49. Jour. of Automated Reasoning, 1997.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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