Peter Padawitz  @ NUS Home/Search
Context Related
| issan.cs.unidortmund.de/...ifipbook.ps Cached: PS.gz PS PDF Image Update Help From: issan.cs.unidortmund.de/~pete... (more) (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: Introduction This chapter deals with the verification of data types. We put particular emphasis on ffl a uniform syntax for constructor-based specifications of both visible and hidden data types, ffl Gentzen clauses, rules and proofs as a uniform schema for presenting (proofs of) conjectures in a natural, flexible, structured and implementable way that keeps the gap between informal reasoning and formal deduction as small as possible, ffl a simple model- and proof-theoretical basis to which ... (Update)
Context of citations to this paper: More
.... 3 Implicational specifications For interpreting implicational specifications we add a rule of 8 introduction to the cut calculus used in [16 18] and generalize the corresponding inference relation according to the rule set induction schema presented in [1] Definition 3.1 Let...
Cited by: More
Modular Swinging Types - Padawitz (1999) (Correct)
Active bibliography (related documents): More All
2.7: Swinging Data Types - The dielectic between actions and.. - Padawitz (1998) (Correct)
1.1: Inductive Theorem Proving for Design Specifications - Padawitz (1997) (Correct)
0.7: Algebraic System Specification and Development.. - Cerioli, Gogolla, .. (1997) (Correct)
Similar documents based on text: More All
0.3: Basic Inference Rules for Algebraic and Coalgebraic Specifications - Padawitz (2002) (Correct)
0.3: Paramorphisms - Meertens (1990) (Correct)
0.2: Computing Rectangular Dissections - A Case Study in Deriving.. - Padawitz (1996) (Correct)
BibTeX entry: (Update)
P. Padawitz, Proof in Flat Specifications, in [2] http://citeseer.comp.nus.edu.sg/242611.html More
@misc{ padawitz-proof,
author = "P. Padawitz",
title = "Proof in Flat Specifications",
text = "P. Padawitz, Proof in Flat Specifications, in [2]",
url = "citeseer.comp.nus.edu.sg/242611.html" }
Citations (may not include all citations):435 Towards a theory of declarative knowledge (context) - Apt, Blair et al. - 1988
392 A Computational Logic (context) - Boyer, Moore - 1979
362 ML for the Working Programmer (context) - Paulson - 1996
313 Inductive logic programming: Theory and methods - Muggleton, de Raedt - 1994
268 Larch: Languages and Tools for Formal Specification (context) - Guttag, Horning - 1993
267 A note on inductive generalization (context) - Plotkin - 1970
254 The integration of functions into logic programming: From th.. (context) - Hanus - 1994
224 Algebraic specification (context) - Wirsing - 1990
202 Modal and temporal logics (context) - Stirling - 1992
192 Logic programming (context) - Apt - 1990
186 Universal coalgebra: A theory of systems - Rutten - 1996
182 Structured operational semantics and bisimulation as a congr.. (context) - Groote, Vaandrager - 1992
177 Fundamentals of Algebraic Specification 1: Equations and Ini.. (context) - Ehrig, Mahr - 1985
171 A needed narrowing strategy - Antoy, Echahed et al. - 1994
168 Rippling: A heuristic for guiding inductive proofs - Bundy, Stevens et al. - 1993
126 Canonical forms and unification (context) - Hullot - 1980
121 An approach to object semantics based on terminal coalgebras (context) - Reichel - 1995
114 Building-in equational theories (context) - Plotkin - 1972
103 Automated deduction by theory resolution - Stickel - 1985
93 Towards an algebraic semantics for the object paradigm - Goguen, Diaconescu - 1994
78 A demand driven computation strategy for lazy narrowing - Loogen, Fraguas et al. - 1993
72 EATCS Bulletin (context) - Jacobs, Rutten et al. - 1997
71 Conditional rewrite rules: Confluence and termination (context) - Bergstra, Klop - 1986
69 induction and computability (context) - Meseguer, Goguen - 1985
69 Handbook of Logic in Computer Science (context) - Abramsky, Gabbay et al. - 1992
65 Automated theorem-proving for theories with simplifiers (context) - Slagle - 1974
50 Proving properties of programs by structural induction (context) - Burstall - 1969
47 volume 828 of Lecture Notes in Computer Science (context) - Paulson, theorem - 1994
45 Proof by consistency (context) - Kapur, Musser - 1987
44 An operational semantics for CSP (context) - Plotkin - 1983
43 Science of Computer Programming (context) - Bidoit, Hennicker et al. - 1995
42 Term rewriting induction (context) - Reddy - 1990
40 Fixpoint induction and proofs of program properties (context) - Park - 1969
39 Fixed point theorems and semantics: A folk tale (context) - Lassez, Nguyen et al. - 1982
38 On completeness of narrowing strategies (context) - Echahed - 1988
38 Canonical conditional rewrite systems (context) - Dershowitz, Okada et al. - 1988
38 Proof systems for hennessy-milner logic with recursion (context) - Larsen - 1988
35 Simplifying conditional term rewriting systems: Unification (context) - Kaplan - 1987
34 Automatic proofs by induction in theories without constructo.. (context) - Jouannaud, Kounalis - 1989
32 Final algebra semantics and data type extensions (context) - Wand - 1979
32 Confluence of conditional rewrite systems (context) - Dershowitz, Okada et al. - 1988
30 Context induction: A proof principle for behavioural abstrac.. (context) - Hennicker - 1991
29 Termination proofs of well-moded logic programs via conditio.. (context) - Ganzinger, Waldmann - 1993
28 Observability concepts in abstract data type specifications (context) - Giarratana, Gimona et al. - 1976
27 Computing in Horn Clause Theories (context) - Padawitz - 1988
26 Partial abstract types (context) - Broy, Wirsing - 1982
26 Guiding induction proofs (context) - Hutter - 1990
25 Towards the one-tiered design of data types and transition s.. (context) - Padawitz - 1998
22 Automated mathematical induction - Bouhoula, Kounalis et al. - 1995
21 Mechanizing inductive reasoning (context) - Kounalis, Rusinowitch - 1990
20 Completion-time optimization of rewritetime goal solving (context) - Bertling, Ganzinger - 1989
19 Level-confluence of conditional rewrite systems with extra v.. - Suzuki, Middeldorp et al. - 1995
19 Conditional rewriting modulo a built-in algebra (context) - Avenhaus, Becker - 1992
18 Inductive completion by ground proof transformation (context) - Kuchlin - 1989
15 On conditional rewrite systems with extra variables and dete.. (context) - Avenhaus, Lor'ia-S'aenz - 1994
14 Parametrized data types do not need highly constrained param.. (context) - Arbib, Manes - 1982
14 Higher-order generalization in program derivation (context) - Pettorossi, Skowron - 1987
12 Analysis of residuating logic programs (context) - Hanus - 1995
12 Reductive conditional term rewriting systems (context) - Jouannaud, Waldmann - 1986
12 Deduction and Declarative Programming (context) - Padawitz - 1992
11 Technical Report CS (context) - Goguen, Malcolm et al. - 1997
7 Inductive theorem proving for design specifications - Padawitz - 1996
6 Expander: A system for testing and verifying functionallogic.. (context) - Padawitz - 1994
6 Subgoal induction (context) - Morris, Wegbreit - 1977
6 Inductive expansion: A calculus for verifying and synthesizi.. (context) - Padawitz - 1991
6 Algebraic specifications of reachable higher-order algebras (context) - Moller, Tarlecki et al. - 1988
5 Handling function definitions through innermost superpositio.. (context) - Fribourg - 1985
5 Bisimulation in algebraic specifications (context) - Astesiano, Wirsing - 1989
5 A recursion planning analysis of inductive completion - Barnett, Basin et al. - 1994
3 Another recursion induction principle (context) - Morris - 1971
2 Final data type specifications: A new data type specificatio.. (context) - Kamin - 1983
1 volume 755 of Lecture Notes in Computer Science (context) - Moller, Partsch et al. - 1993
1 German course notes (context) - Padawitz, programming - 1997
Documents on the same site (http://issan.cs.uni-dortmund.de/~peter/): More
Inductive Theorem Proving for Design Specifications - Padawitz (1997) (Correct)
Modular Swinging Types - Padawitz (1999) (Correct)
Modular Swinging Types - Padawitz (1999) (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.