Schriftenverzeichnis¹

Journal- und Buchbeiträge

-

C.Kreitz & S.Schmitt. A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems, Journal of Information and Computation.   (erscheint Anfang 2000)

-

C.Kreitz, J.Otten, S.Schmitt, B.Pientka. Matrix-based Constructive Theorem Proving. In Intellectics and Computational Logic. Papers in honor of Wolfgang Bibel, Kluwer, April 2000.

-

B.Pientka & C.Kreitz. Automating inductive Specification Proofs, Fundamenta Informatica
39(1-2):189-209, 1999.

-

C.Kreitz & J.Otten. Connection-based Theorem Proving in Classical and Non-classical Logics, Journal for Universal Computer Science 5(3):88-112, Springer-Verlag, 1999.

-

C.Kreitz. Program Synthesis. In Automated Deduction - A Basis for Applications, Kapitel III.2.5, pp.105-134, Kluwer, 1998.

-

C.Kreitz. Projektaufgaben in Anfängerveranstaltungen: ein Mittel zur Förderung eines objektorientierten Programmierstils. GI Softwaretechnik-Trends, 16(4):30-43, 1996.

-

C.Kreitz. Formal Mathematics for Verifiably Correct Program Synthesis. Journal of the Interest Group in Pure and Applied Logics (IGPL), 4(1):75-94, 1996.

-

K.Weihrauch & C.Kreitz. Type 2 computational complexity of functions on Cantor's space. Theoretical Computer Science, 82:1-18, 1991.

-

C.Kreitz. Towards a formal theory of program construction. Revue d' intelligence artificielle, 4(3):53-79, 1990.

-

C.Kreitz & K.Weihrauch. Compactness in constructive analysis revisited. Annals of pure and applied logic, 36:29-38, 1987.

-

K.Weihrauch & C.Kreitz. Representations of the real numbers and the open subsets of the set of real numbers. Annals of pure and applied logic, 35:247-260, 1987.

-

C.Kreitz & K.Weihrauch. Theory of representations. Theoretical Computer Science, 38:35-53, 1985. 79

Tagungsbeiträge

-

S.Allen, R.Constable, R.Eaton, C.Kreitz, L.Lorigo. The Nuprl Open Logical Environment, 17^th International Conference on Automated Deduction, LNAI , Springer, 2000.

-

C.Kreitz, & B.Pientka. Matrix-based Inductive Theorem Proving, International Conference
TABLEAUX-2000, LNAI, Springer, 2000.

-

K.Birman, B.Constable, M.Hayden, J.Hickey, C.Kreitz, R.van Renesse, O.Rodeh, W.Vogels. The Horus and Ensemble Projects: Accomplishments and Limitations. DISCEX'00, 2000.

-

X.Liu, C.Kreitz, R.van Renesse, J.Hickey, M.Hayden, K.Birman, R.Constable. Building Reliable, High-Performance Systems from Components, 17^th ACM Symposium on Operating System Principles (SOSP'99), Operating Systems Review 34(5):80-92, Dezember 1999.

-

C.Kreitz. Automated Fast-Track Reconfiguration of Group Communication Systems, 5^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1579, pp.104-118, Springer, 1999.

-

H.Mantel & C.Kreitz. A Matrix Characterization for MELL, 6^th European Workshop on Logics in Artificial Intelligence, European Workshop, JELIA '98, LNAI 1489, pp.169-183, Springer, 1998.

-

B.Pientka & C.Kreitz. Instantiation of existentially quantified variables in inductive specification proofs, 4^th International Conference on Artificial Intelligence and Symbolic Computation, LNAI 1476, pp.247-258, Springer, 1998.

-

C.Kreitz, M.Hayden & J.Hickey. A Proof Environment for the Development of Group Communication Systems, 15^th International Conference on Automated Deduction, LNAI 1421, pp.317-332, Springer, 1998.

-

S.Schmitt & C.Kreitz. Deleting Redundancy in Proof Reconstruction, International Conference TABLEAUX-98, LNAI 1397, pp.262-276, Springer, 1998.

-

W.Bibel, D.Korn, C.Kreitz, F.Kurucz, J.Otten, S.Schmitt & G.Stolpmann. A multi-level approach to program synthesis. 7^th International Workshop on Logic Program Synthesis and Transformation, LNAI 1463, pp.1-25, Springer, 1998.

-

D.Korn & C.Kreitz. Deciding Intuitionistic Propositional Logic via Translation into Classical Logic, 14^th International Conference on Automated Deduction, LNAI 1249, pp.131-145, Springer, 1997.

-

C.Kreitz, H.Mantel, J.Otten & S.Schmitt. Connection-Based Proof Construction in Linear Logic, 14^th International Conference on Automated Deduction, LNAI 1249, pp.207-221, Springer, 1997.

-

J.Otten & C.Kreitz. A Uniform Proof Procedure for Classical and Non-classical Logics. KI-96: Advances in Artificial Intelligence, LNAI 1137, pp.307-319, Springer, 1996.

-

W.Bibel, D.Korn, C.Kreitz, S.Schmitt. Problem-Oriented Applications of Automated Theorem Proving. 4^th International Symposium on Design and Implementation of Symbolic Computation Systems, LNCS 1128, pp.1-21, Springer, 1996.

-

S.Schmitt & C.Kreitz. Converting Non-Classical Matrix Proofs into Sequent-Style Systems. 13^th International Conference on Automated Deduction, LNAI 1104, pp.418-432, Springer, 1996.

-

C.Kreitz, K.Lau, M.Ornaghi. Formal Reasoning about Modules, Reuse, Objects, and their Correctness. International Conference on Formal and Applied Practical Reasoning, LNAI 1085, pp.384-398, Springer, 1996.

-

J.Otten & C.Kreitz. T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods. 5^th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 1071, pp.244-260, Springer, 1996.

-

C.Kreitz, J.Otten, S.Schmitt. Guiding Program Development Systems by a Connection Based Proof Strategy. 5^th International Workshop on Logic Program Synthesis and Transformation, LNCS 1048, pp.137-151, Springer, 1996.

-

S.Schmitt & C.Kreitz. On Transforming Intuitionistic Matrix Proofs into Standard-Sequent Proofs. 4^th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918, pp.106-121, Springer, 1995.

-

J.Otten & C.Kreitz. A Connection Based Proof Method for Intuitionistic Logic. 4^th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918, pp.122-137, Springer, 1995.

-

T.Boy de la Tour & C.Kreitz. Building proofs by Analogy via the Curry-Howard Isomorphism. Conference on Logic Programming and Automated Reasoning, LNAI 624, pp.202-213. Springer, 1992.

-

C.Kreitz. The representation of program synthesis in higher order logic. 14^th German Workshop on Artificial Intelligence, IFB 251, pp.171-180. Springer, 1990.

-

G.Neugebauer, B.Fronhöfer, C.Kreitz. XPRTS - an implementation tool for program synthesis. 13^th German Workshop on Artificial Intelligence, IFB 216, pp.348-357. Springer, 1989.

-

C.Kreitz & K.Weihrauch. Towards a theory of representations. 2^nd Frege Conference, pp.73-79, Akademie Verlag, 1984.

-

C.Kreitz & K.Weihrauch. A unified approach to constructive and recursive analysis. Computation and proof theory, LNM 1104, pp.259-278. Springer, 1984.

-

C.Kreitz & K.Weihrauch. Complexity theory on real numbers and functions. 6^th GI conference on Theoretical Computer Science, LNCS 145, pp.165-174. Springer, 1982.

Neuere Technische Berichte

-

H.Mantel & C.Kreitz. A Matrix Characterization for Multiplicative Exponential Linear Logic, Technical Report, Cornell University, Ithaca, NY, März 2000.

-

C.Kreitz. Formal Reasoning about Communication Systems II: Automated Fast-Track Reconfiguration. Technical Report TR98-1707, Cornell University, Ithaca, NY, September 1998.

-

O.Hafizogullari & C.Kreitz. A Type-based Framework for Automatic Debugging, Technical Report, Cornell University, Ithaca, NY, Juli 1998.

-

O.Hafizogullari & C.Kreitz. Dead Code Elimination Through Type Inference Technical Report TR 98-1698, Cornell University, Ithaca, NY, März 1998.

-

C.Kreitz. Formal Reasoning about Communication Systems I: Embedding ML into Type Theory. Technical Report TR 97-1637, Cornell University, Ithaca, NY, Juli 1997.

Akademische Abschlußarbeiten

-

Metasynthesis - Deriving Programs that Develop Programs. Habilitationsschrift, Technische Universität Darmstadt, 1992. Forschungsbericht AIDA-93-03, TU Darmstadt, FG Intellektik. tex2html_deferred

-

Theorie der Darstellungen und ihre Anwendungen in der konstruktiven Analysis. Dissertation, FernUniversität Hagen, 1984. Informatik-Berichte 50. FernUniversität Hagen.

-

Zulässige CPO's - ein Entwurf für ein allgemeines Berechenbarkeitskonzept. Diplomarbeit, RWTH Aachen, 1981. Schriften zur Mathematik und angewandten Informatik 76, RWTH Aachen.

Beiträge auf Workshops

-

O.Hafizogullari & C.Kreitz. Dependency Analysis Through Type Inference. 6^th Workshop on Logic, Language, Information and Computation (WoLLIC'99), Rio de Janeiro, Brazil 1999.

-

D.Korn & C.Kreitz. A Constructively Adequate Refutation System for Intuitionistic Logic. 6^th International Conference TABLEAUX'97 - Short Papers, Technical Report CRIN 97-R-030, Université de Nancy II, 1997.

-

C.Kreitz, J.Otten, S.Schmitt. Integrating a Connection Based Proof Method into an Interactive Program Development System. ProCos Workshop on Linking Theories, Vedbaek, 1995.

-

D.Korn & C.Kreitz. On Testing Irreflexivity of Reduction Orderings for Combined Substitutions in Intuitionistic Matrix Proofs. 4^th Workshop on Theorem Proving with Analytic Tableaux and Related Methods - Short Papers & Poster Sessions, Universität Koblenz, pp.55-60, 1995.

-

C.Kreitz. Das Grundstudium an der TH Darmstadt aus studentischer Sicht - Analyse einer fachübergreifenden Umfrage. 2.THD Werkstattgespräch zur Verbesserung der Lehre, Darmstadt, THD Schriftenreihe Wissenschaft und Technik 67, pp.81-105, 1995.

-

C.Kreitz. Förderung des Guten - Änderung des Schlechten: 5 Thesen zur Verbesserung der Grundlehre an der TH Darmstadt. 2.THD Werkstattgespräch zur Verbesserung der Lehre, Darmstadt, THD Schriftenreihe Wissenschaft und Technik 67, pp.107-117, 1995.

Skripten und Konzeptpapiere

-

A.Blunck, M.Heger, G.Hellmann, C.Kreitz & B.Pollak. Lehr- und Lernformen in Studiengängen, TU Darmstadt, Hochschuldidaktische Arbeitsstelle, 1995.

-

C.Kreitz. Automatisierte Logik und Programmierung I+II, Skriptum zur Vorlesung, Wintersemester 1994/95 + Sommersemester 1995, 350 Seiten.

-

C.Kreitz. Lernen im Grundstudium: Orientierung - Beratung - Tutorien - Prüfungen. Protokoll des Workshops ``Lernen im Grundstudium'', 2.THD Werkstattgespräch zur Verbesserung der Lehre, Darmstadt, Juli 1994, THD Schriftenreihe Wissenschaft und Technik 67, pp.51-57, 1995.

-

C.Kreitz. Grundlagen der Informatik I: Programmierung, Skriptum zur Vorlesung, Wintersemester 1993/94, 200 Seiten.

-

C.Kreitz. Grundlagen der Informatik IV: Theoretische Informatik, Skriptum zum Repetitorium, September 1993, 40 Seiten

-

W.Henhapl, U.Andelfinger, W.Bender, C.Kreitz: Konzeption eines Nebenfachstudiums ``Sozialorientierte Gestaltung von Informationstechnik'', TU Darmstadt, 1992.

<985>>