David A. Basin  @ NUS Home/Search
Context Related
| informatik.unifreiburg.d...iclp11.ps.Z Cached: PS.gz PS PDF Image Update Help From: informatik.unifreiburg.de...pubs (more) (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: The Whelk logic has been proposed as a foundation for logic program synthesis. Here, I interpret the rules of Whelk as rules of first-order logic and derive them in Isabelle. Theoretically, this provides a means to understand the meta-theory behind Whelk, and its correctness. The interpretation suggests simplifications, corrections, and extensions. Practically, it provides a way to construct logic programs from proofs of their correctness by applying the formalized proof rules using... (Update)
Context of citations to this paper: More
.... a formal guarantee of the correctness of the calculi and helped us find and correct errors in calculi proposed by other researchers [Basin 1994]. Third, although it sometimes requires considerable work to reinterpret development calculi as collections of derived rules (see...
Cited by: More
Logical Framework Based Program Development - Basin (1998) (Correct)
Similar documents (at the sentence level):
11.1%: Logic Frameworks for Logic Programs - Basin (1994) (Correct)
Active bibliography (related documents): More All
0.3: Logic Program Schemata: Synthesis and Analysis - Flener (1995) (Correct)
0.3: Logic Program Synthesis - Deville, Lau (1993) (Correct)
0.2: Program Development Schemata as Derived Rules - Anderson, Basin (1998) (Correct)
Similar documents based on text: More All
0.7: Guiding Synthesis Proofs - Lombart, Wiggins, Deville (1993) (Correct)
0.2: CompuNet subgroup on Program Development, Analysis and.. - Bruynooghe, al. (1995) (Correct)
0.1: Sound And Complete Translations From Sorted Higher-Order Logic.. - Kerber (1994) (Correct)
BibTeX entry: (Update)
Basin, D. 1994. Isawhelk: Whelk interpreted in Isabelle. In 11th International Conference on Logic Programming (ICLP94) (1994). http://citeseer.comp.nus.edu.sg/119188.html More
@misc{ basin94isawhelk,
author = "D. Basin",
title = "Isawhelk: Whelk interpreted in Isabelle",
text = "Basin, D. 1994. Isawhelk: Whelk interpreted in Isabelle. In 11th International
Conference on Logic Programming (ICLP94) (1994).",
year = "1994",
url = "citeseer.comp.nus.edu.sg/119188.html" }
Citations (may not include all citations):392 A Computational Logic (context) - Boyer, Moore - 1979
251 A logic programming language with lambda-abstraction - Miller - 1991
210 Logic programming in the LF logical framework - Pfenning - 1991
163 Application of theorem proving to problem solving (context) - Green - 1969
150 Edinburgh LCF: A Mechanized Logic of Computation (context) - Gordon, Milner et al. - 1979
145 Isabelle: the next 700 theorem provers (context) - Paulson - 1990
129 The foundation of a generic theorem prover - Paulson - 1989
38 Introduction to Isabelle (context) - Paulson - 1993
31 Isabelle's object-logics - Paulson - 1993
30 The synthesis of logic programs from inductive proofs (context) - Bundy, Smaill et al. - 1990
28 A first order theory of data and programs (context) - Clark, Tarnlund - 1977
28 Logic program synthesis via proof planning - Kraan, Basin et al. - 1992
28 Middle-out reasoning for logic program synthesis - Kraan, Basin et al. - 1993
17 Synthesis and transformation of logic programs in the Whelk .. (context) - Wiggins - 1992
14 Predicate Logic: a calculus for deriving programs (context) - Clark, Sickel - 1977
11 schema-guided synthesis of logic programs (context) - Flener, Deville - 1991
11 A framework for program development based on schematic proof - Basin, Bundy et al. - 1993
6 Formal validation of transformation schemata (context) - Waldau - 1991
5 Term rewriting and beyond --- theorem proving in Isabelle (context) - Nipkow - 1989
2 A conservative extension of first order logic and its applic.. (context) - Basin, Matthews - 1993
Documents on the same site (http://www.informatik.uni-freiburg.de/~basin/pubs/pubs.html): More
A Modular Presentation of Modal Logics in a Logical.. - Basin, Matthews.. (Correct)
A Recursion Planning Analysis of Inductive Completion - Barnett, Basin, Hesketh (1994) (Correct)
Program Development Schemata as Derived Rules - Anderson, Basin (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.