Serge Autexier  @ NUS Home/Search
Context Related
| dfki.de/~serge/pub/phdthesis.ps.gz Cached: PS.gz PS PDF Image Update Help From: dfki.de/~serge/...blicationsmain (more) (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: VII Zusammenfassung IX Extended Abstract XI Acknowledgements XIII I (Update)
Cited by: More
Interactive Theorem Proving with Tasks - Hübner, Autexier, Benzmüller, Meier (2003) (Correct)
Assertion Application in Theorem Proving and Proof Planning - Vo, Benzmüller, Autexier (2003) (Correct)
Active bibliography (related documents): More All
0.7: Towards an Evolutionary Formal Software Development - Hutter, Schairer (1999) (Correct)
0.7: Equational Proof-Planning by Dynamic Abstraction - Autexier, Hutter (1997) (Correct)
0.7: A Framework for Generic and Reusable Tactics - Autexier (1999) (Correct)
Similar documents based on text: More All
0.6: Superposition Theorem Proving for Commutative Algebraic Theories - Stuber (2000) (Correct)
0.6: Cryptographically Sound Analysis of Security Protocols - Backes (2002) (Correct)
0.6: Secure Group Key Agreement - Steiner (2002) (Correct)
Related documents from co-citation: More All
2: Reconstructing proofs at the assertion level - Huang - 1994
2: A proof-planning framework with explicit abstractions based on indexed formulas - Autexier - 2001
BibTeX entry: (Update)
S. Autexier. Hierarchical Contextual Reasoning. PhD Thesis, Saarland University, forthcoming. http://citeseer.comp.nus.edu.sg/684610.html More
@misc{ autexier-hierarchical,
author = "S. Autexier",
title = "Hierarchical Contextual Reasoning",
text = "S. Autexier. Hierarchical Contextual Reasoning. PhD Thesis, Saarland University,
forthcoming.",
url = "citeseer.comp.nus.edu.sg/684610.html" }
Citations (may not include all citations):729 The Lambda Calculus -- Its Syntax and Semantics (context) - Henk - 1984
634 A machine oriented logic based on the resolution principle (context) - John - 1965
434 A framework for defining logics - Robert, Furio et al. - 1987
430 Structure and Interpretation of Computer Programs (context) - Abelson, Sussman et al. - 1996
419 A formulation of the simple theory of types (context) - Alonzo - 1940
392 A computational logic (context) - Robert, Moore et al. - 1979
353 Term Rewriting and All That (context) - Franz, Tobias - 1998
235 First-Order Logic (context) - Smullyan - 1968
226 The use of explicit plans to guide inductive proofs - Alan - 1988
176 Notes on formalizing context - Jon, September - 1993
172 Higher order abstract syntax (context) - Frank, Conal - 1988
157 Edinburgh LCF -- A mechanised logic of computation (context) - Gordon, Milner et al. - 1979
151 An Introduction to Mathematical Logic and Type Theory: To Tr.. (context) - Peter - 2002
142 Logic programming with focusing proofs in linear logic - Jean-Marc - 1992
136 System description: Twelf - a meta-logical framework for ded.. - Frank, urmann - 1999
134 Unification Theory - Siekmann - 1987
129 The foundation of a generic theorem prover - Lawrence - 1989
126 Higher-order critical pairs (context) - Tobias - 1991
107 A New Introduction to Modal Logic (context) - Hughes, Cresswell - 1996
87 The Oyster-Clam system (context) - Bundy, van Harmelen et al. - 1990
86 Completeness in the theory of types (context) - Leon - 1950
86 Implementing Mathematics with the Nuprl Development System (context) - Robert, Allen et al. - 1986
74 Basic paramodulation and superposition (context) - Leo, Harald et al. - 1992
73 Theorem proving via general matings (context) - Peter, April - 1981
63 Theorem Proving with Abstractions (context) - David - 1981
56 Higherorder unification revisited: Complete sets of transfor.. (context) - Wayne, Jean et al. - 1989
51 Recherches sur la th eorie de la d emonstration (context) - Jacques - 1930
50 An unsolvable problem of elementary number theory (context) - Alonzo - 1936
46 Paradigms of Artificial Intelligence Programming: Case Studi.. (context) - Peter - 1992
43 A many-sorted calculus based on resolution and paramodulatio.. (context) - Christoph - 1987
43 A survey of the project AUTOMATH (context) - Nicolaas - 1980
41 Integrating computer algebra into proof planning - Manfred, Michael et al. - 1998
36 On computable numbers (context) - Alan - 1937
36 Formalizing a hierarchical structure of practical mathematic.. (context) - Peter, Staples - 1993
34 Extension to the rippling-out tactic for guiding inductive p.. (context) - Bundy, van Harmelen et al. - 1990
32 The practice of logical frameworks - Frank - 1996
31 INKA - The Next Generation - Dieter, Claus - 1996
31 A semi-functional implementation of a higher-order logic pro.. - Conal, Frank - 1991
30 The TPS Theorem Proving System (context) - Peter, Issar et al. - 1990
29 Integration of automated and interactive theorem proving in .. (context) - Bernd, Gehne et al. - 1997
28 Proofs in Higher-Order Logic (context) - Dale - 1983
28 eine der arithmetischen nachgebildete Formelsprache des rein.. (context) - Gottlob
27 Principia Mathematica (context) - Alfred, Russell - 1910
26 Guiding induction proofs (context) - Dieter - 1990
24 Theorem proving modulo - Gilles, Th et al. - 1998
23 Proof Transformation in Higher-Order Logic (context) - Frank - 1987
23 A window inference tool for refinement (context) - Jim - 1992
23 Der Wahrheitsbegriff in den formalisierten Sprachen (context) - Alfred - 1936
22 Higher-order narrowing - Christian - 1994
20 Window inference in the HOL system (context) - Jim - 1991
20 Xbarnacle: Making theorem provers more accessible - David, Helen - 1997
20 string unification: Unifying prefixes in non-classical proof.. (context) - Jens, Christoph - 1996
19 Human Oriented Proof Presentation: A Reconstructive Approach - Xiaorong - 1994
18 SPASS: Combining Superposition (context) - Christoph - 1999
18 Proof Theory (context) - utte - 1977
16 Colouring terms to control equational reasoning - Dieter - 1997
16 System description: Inka (context) - Serge, Dieter et al. - 1999
15 On implementing prolog in functional programming (context) - Carlsson - 1984
15 The Clausal Theory of Types (context) - David - 1993
15 Theorem proving in cancellative abelian monoids - Harald, Uwe - 1996
15 Automated proof search in non-classical logics: efficient ma.. (context) - Lincoln - 1990
15 Tableau methods of proof for modal logics (context) - Melvin - 1972
14 A system of axiomatic set-theory (context) - Paul - 1937
14 A system of axiomatic set-theory (context) - Paul - 1941
12 Activemath: A generic and adaptive web-based learning enviro.. - Erica, es et al. - 2001
12 Logic of demonstratives (context) - Kaplan - 1978
11 A Resolution-Based Calculus for Temporal Logics (context) - Andreas - 1995
11 The Consistency of the Axiom of Choice and of the Generalize.. (context) - odel - 1940
11 Inference with path resolution and semantic graphs (context) - Neil, Rosenthal et al. - 1987
11 the Representation of Mathematical Concepts and their Transl.. (context) - Manfred - 1992
10 Mbase: Representing mathematical knowledge in a relational d.. (context) - Andreas, Michael - 1999
10 On automating diagrammatic proofs of arithmetic arguments - Mateja, Alan et al. - 1999
10 Untersuchungen uber die Grundlagen der Mengenlehre (context) - Ernst - 1908
9 The discoveries of continuations - Reynolds - 1993
7 Presenting proofs in a human-oriented way (context) - Helmut - 1999
7 Formal software development in the KIV system (context) - Heisel, Reif et al. - 1991
7 On Lisp -- Advanced Techniques for Common Lisp (context) - Graham - 1994
7 ABSFOL: A proof checker with abstraction (context) - Fausto, Adolfo - 1996
6 VSE: Formal methods meet industrial needs - Autexier, Hutter et al. - 1998
5 The Markgraf Karl Refutation procedure (context) - Norbert, Hans-J - 1986
5 System Description: TPS: A Theorem Proving System for Type T.. - Peter, Bishop et al. - 2000
5 Window inference in isabelle - Mark - 1995
4 The development graph manager MAYA - Serge, Dieter et al. - 2002
4 A pragmatic approach to reuse in tactical theorem proving - Axel, Serge et al. - 2001
4 Equational proof-planning by dynamic abstraction - Serge, Dieter - 1997
4 Automation of diagrammatic reasoning - Mateja, Alan et al. - 1997
4 Zu den Grundlagen der CantorZermeloschen Mengenlehre (context) - Adolf - 1922
3 User-adaptive Proof Explanation (context) - Armin - 2001
3 Introduction to Combinators and l-Calculus (context) - Hindley, Roger - 1986
3 System Description: TRAMP: Transformation of Machine-Found P.. - Andreas - 2000
3 Special Issue on Strategies in Automated Deduction (context) - Dieter, reasoning et al. - 2000
3 Equalizing terms by difference reduction techniques - Dieter - 1997
3 A Matrix Characterization for MELL - Heiko, Christoph - 1998
3 Intuitionism and Formalism (context) - Luitzen - 1914
3 Focussing and proof construction - Jean-Marc - 2000
2 An abstraction for proof-planning: The S-abstraction - Serge - 1997
2 Synthesizing induction orderings for existence proofs (context) - Dieter - 1994
2 Die Vollst andigkeit der Axiome des logischen Funktionenkalk.. (context) - odel - 1930
2 General models (context) - Peter, June - 1972
2 Proof Planning with Multiple Strategies (context) - Andreas - 2003
2 Human-readable machine-verifiable proofs for teaching constr.. - Andreas, Bor-Yuh et al. - 2001
1 Semantic techniques for cut-elimination in higher order logi.. (context) - uller, Kohlhase et al. - 2002
1 On connections in higher-order logic (context) - Peter - 1989
1 The foundations of mathematics : a study in the philosophy o.. (context) - Evert - 1965
1 Probleme der Grundlegung der Mathematik (context) - David - 1930
1 Reprinted by Basil Blackwell (context) - George, Analysis et al. - 1965
1 Fast decision algorithms based on union and find (context) - Greg, Derek et al. - 1977
1 Die Axiomatisierung der Megenlehre (context) - John - 1928
1 Supporting interactive theorem proving in CORE (context) - ubner - 2003
1 Path dissolution: A strongly complete inference rule (context) - Neil, Rosenthal et al. - 1987
1 OANTS -- an open approach at combining interactive and autom.. (context) - uller, Sorge et al. - 2000
1 LWUI: Lovely Wmega user interface (context) - Siekmann - 1999
1 Higher Order Semantics and Extensionality (context) - uller, Kohlhase et al. - 2002
1 Rippling: Meta-Level Guidance for Mathematical Reasoning (context) - Alan, David et al. - 2003
1 Uber formal entscheidbare S atze der Principia Mathematica u.. (context) - odel - 1931
1 TAS and IsaWin: Tools for transformational program developme.. - uth, Tej et al. - 1999
1 Automated theorem proving in first-order logic modulo: on th.. (context) - Gilles - 2000
1 Zur Begr undung der intuitionistischen Mathematik (context) - Luitzen - 1925
1 eminaire de Math ematiques Superieures (context) - Nicolaas, AUTOMATH et al. - 1973
Documents on the same site (http://www.dfki.de/~serge/s.cgi?publications-main.html): More
Parameterized Abstractions used for Proof-Planning - Autexier, Hutter (1997) (Correct)
System Description: inka 5.0 - A Logic Voyager - Autexier, Hutter, Mantel.. (1999) (Correct)
Simultaneous Quantifier Elimination - Autexier, Mantel, Stephan (1998) (Correct)
Online articles have much greater impact More about CiteSeer.IST at NUS Add search form to your site Submit documents Feedback
CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.