Skip to main content
SpringerLink
Log in

Logic program synthesis by induction over Horn Clauses

  • Conference paper
  • First Online:
Logic Program Synthesis and Transformation (LOPSTR 1995)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1048))

  • 162 Accesses

Abstract

We report on the implementation of a new induction scheme in the Whelk logic program synthesis and transformation system [5]. The scheme is based on work by Feferman [1], and allows constructive proof by induction over the minimal Herbrand model of a set of Horn Clauses. This is an important addition to the Whelk system, because it admits reasoning about and synthesis from “real” logic programs, whereas previously the system was limited to induction over recursive data structures.

The contribution of this work is practical, in the extension of the synthesis capability of the Whelk program synthesis system. Theoretically, it is closely related to an extension of [2] (reported in [3]), where a similar induction scheme is used to synthesise logic programs which embody functions.

Full details of the extension and its implementation may be found in [4].

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

References

  1. S. Feferman. Finitary inductively presented logics. In Logic Colloquium '88, pages 191–220, Amsterdam, 1989. North-Holland.

    Google Scholar 

  2. L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In Proceedings of Eighth International Conference on Logic Programming, pages 685–699. MIT Press, June 1990. Extended version in [3].

    Google Scholar 

  3. J.-M. Jacquet, editor. Constructing Logic Programs. Wiley, 1993.

    Google Scholar 

  4. A. J. Parkes. Generator induction for relational proofs, logic programming and reasoning about database systems. MSc dissertation, Dept. of Artificial Intelligence, Edinburgh, 1994.

    Google Scholar 

  5. G. A. Wiggins. Synthesis and transformation of logic programs in the Whelk proof development system. In K. R. Apt, editor, Proceedings of JICSLP-92, pages 351–368. M.I.T. Press, Cambridge, MA, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CIRL 1268 University of Oregon, 97403-1269, Eugene, OR, USA

    Andrew J. Parkes

  2. Department of Artificial Intelligence, University of Edinburgh, 80 South Bridge, EH1 1HN, Edinburgh, Scotland

    Geraint A. Wiggins

Authors
  1. Andrew J. Parkes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Geraint A. Wiggins
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Maurizio Proietti

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Parkes, A.J., Wiggins, G.A. (1996). Logic program synthesis by induction over Horn Clauses. In: Proietti, M. (eds) Logic Program Synthesis and Transformation. LOPSTR 1995. Lecture Notes in Computer Science, vol 1048. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60939-3_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-60939-3_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60939-1

  • Online ISBN: 978-3-540-49745-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation