Laurent Fribourg, Hans Olsen  @ NUS Home/Search
Context
Related
| lsv.enscachan.fr/~fribour...olsen92.ps Cached: PS.gz PS PDF Image Update Help From: lsv.enscachan.fr/~fribo...publis (more) (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: In the framework of Extended Prolog Execution [K&S 86] a rule of Structural Induction is presented. For the induction step the new rule takes advantage of a Prolog program synthesized through Proof-Extraction techniques, and rests on extensive use of Negation as Failure Inference for exploiting the information contained in the extracted program. We describe how to synthesize Prolog procedures when applying the inference rule and show that they are guaranteed to preserve partial correctness and... (Update)
Active bibliography (related documents): More All
0.4: Logic Program Synthesis - Deville, Lau (1993) (Correct)
0.4: Searching for Inductive Proofs in Second-Order Intuitionistic.. - McCarty (1992) (Correct)
0.2: On the Use of Inductive Reasoning in Program Synthesis.. - Flener, Popelínsky (1994) (Correct)
Similar documents based on text: More All
0.1: Proving Safety Properties of Infinite State Systems by.. - Fribourg, Olsén (1996) (Correct)
0.1: Datalog Programs with Arithmetical Constraints: Hierarchic.. - Fribourg, al. (1995) (Correct)
0.1: A Decompositional Approach for Computing Least Fixed-Points.. - Fribourg, Olsen (1996) (Correct)
BibTeX entry: (Update)
@misc{ fribourg-unifying,
author = "Laurent Fribourg and Hans Olsen",
title = "A Unifying View of Structural Induction and Computation Induction for Logic
Programs",
url = "citeseer.comp.nus.edu.sg/66564.html" }
Citations (may not include all citations):759 Negation As Failure (context) - Clark - 1978
229 Theory of Recursive Functions and Effective Computability (context) - Rogers - 1967
78 Predicate Logic as a Computational Formalism (context) - Clark - 1979
50 Proving Properties of Programs by Structural Induction (context) - Burstall - 1969
23 Extracting Logic Programs from Proofs that use Extended Prol.. (context) - Fribourg - 1990
8 Verification of Prolog Programs Using an Extension of Execut.. (context) - Kanamori, Seki - 1986
6 Fixpoint Approach to the Theory of Computation (context) - Manna, Vuillemin - 1972
4 Automatic Generation of Simplification Lemmas for Inductive .. (context) - Fribourg - 1991
1 Laboratoire d'Informatique de l'Ecole Normale Sup'erieure (context) - Bouverot, Extracting - 1991
1 em Automated Inductive Reasoning about Logic Programs (context) - Elkan, McAllester - 1988
1 Induction as the Basis for Program Verification (context) - Reynolds, Yeh - 1976
Documents on the same site (http://www.lsv.ens-cachan.fr/~fribourg/publis.html):
Mixing List Recursion and Arithmetic - Fribourg (1991) (Correct)
Implementation of Narrowing: The Prolog-Based Approach - Cheong, Fribourg (1993) (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.