A Unifying View of Structural Induction and Computation Induction for Logic Programs  (Make Corrections)  
Laurent Fribourg, Hans Olsen

 @ NUS   Home/Search   Context   Related

 
View or download:
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  
(Enter summary)

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.