Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Fixed Points of Functors - A Short Abstract Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Category Theoretic Semantics for Theorem Proving in Logic Programming: Embracing the Laxness

Authors : Ekaterina Komendantskaya, John Power

Published in: Coalgebraic Methods in Computer Science

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

A propositional logic program P may be identified with a \(P_fP_f\)-coalgebra on the set of atomic propositions in the program. The corresponding \(C(P_fP_f)\)-coalgebra, where \(C(P_fP_f)\) is the cofree comonad on \(P_fP_f\), describes derivations by resolution. Using lax semantics, that correspondence may be extended to a class of first-order logic programs without existential variables. The resulting extension captures the proofs by term-matching resolution in logic programming. Refining the lax approach, we further extend it to arbitrary logic programs. We also exhibit a refinement of Bonchi and Zanasi’s saturation semantics for logic programming that complements lax semantics.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Duality of Equations and Coequations via Contravariant Adjunctions
next chapter Product Rules and Distributive Laws
Literature
1.
Amato, G., Lipton, J., McGrail, R.: On the algebraic structure of declarative programming languages. Theor. Comput. Sci. 410(46), 4626–4671 (2009)MathSciNetCrossRefMATH
2.
Benabou, J.: Introduction to bicategories. In: Bénabou, J., Davis, R., Dold, A., Isbell, J., MacLane, S., Oberst, U., Roos, J.-E. (eds.) Reports of the Midwest Category Seminar. Lecture Notes in Mathematics, vol. 47, pp. 1–77. Springer, Heidelberg (1967)
3.
4.
Bonchi, F., Montanari, U.: Reactive systems, (semi-)saturated semantics and coalgebras on presheaves. Theor. Comput. Sci. 410(41), 4044–4066 (2009)MathSciNetCrossRefMATH
5.
Bruni, R., Montanari, U., Rossi, F.: An interactive semantics of logic programming. TPLP 1(6), 647–690 (2001)MathSciNetMATH
6.
Bonchi, F., Zanasi, F.: Saturated semantics for coalgebraic logic programming. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 80–94. Springer, Heidelberg (2013)CrossRef
7.
Bonchi, F., Zanasi, F.: Bialgebraic semantics for logic programming. CoRR abs/1502.06095 (2015)
8.
9.
10.
Fu, P., Komendantskaya, E., Schrijvers, T., Pond, A.: Proof relevant corecursive resolution. In: Kiselyov, O., King, A., et al. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 126–143. Springer, Heidelberg (2016). doi:10.​1007/​978-3-319-29604-3_​9 CrossRef
11.
Jones, S.P., Jones, M., Meijer, E.: Type classes: an exploration of the design space. In: Haskell Workshop (1997)
12.
Gupta, G., Costa, V.: Optimal implementation of and-or parallel prolog. In: PARLE 1992, pp. 71–92 (1994)
13.
Jifeng, H., Hoare, C.A.R.: Categorical semantics for programming languages. In: Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1989. LNCS, vol. 442, pp. 402–417. Springer, Heidelberg (1989)CrossRef
14.
Jifeng, H., Hoare, C.A.R.: Data refinement in a categorical setting. Technical Monograph PRG-90. Oxford University Computing Laboratory, Programming Research Group, Oxford (1990)
15.
Johann, P., Komendantskaya, E., Komendantskiy, V.: Structural resolution for logic programming. In: Technical Communications of ICLP 2015 (2015)
16.
Kelly, G.M.: Coherence theorems for lax algebras and for distributive laws. In: Kelly, G.M. (ed.) Category Seminar. Lecture Notes in Mathematics, vol. 420, pp. 281–375. Spriniger, Heidelberg (1974)CrossRef
17.
Kelly, G.M.: Basic Concepts of Enriched Category Theory. London Math. Soc. Lecture Notes Series, vol. 64. Cambridge University Press, Cambridge (1982)
18.
19.
Kinoshita, Y., Power, J.: A fibrational semantics for logic programs. In: Dyckhoff, R., Herre, H., Schroeder-Heister, P. (eds.) ELP 1996. LNCS (LNAI), vol. 1050, pp. 177–191. Springer, Heidelberg (1996)CrossRef
20.
Komendantskaya, E., McCusker, G., Power, J.: Coalgebraic semantics for parallel derivation strategies in logic programming. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 111–127. Springer, Heidelberg (2011)CrossRef
21.
Komendantskaya, E., Power, J.: Coalgebraic semantics for derivations in logic programming. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 268–282. Springer, Heidelberg (2011)CrossRef
22.
Komendantskaya, E., Power, J.: Coalgebraic derivations in logic programming. In: CSL. LIPIcs, pp. 352–366. Schloss Dagstuhl (2011)
23.
Komendantskaya, E., Power, J., Schmidt, M.: Coalgebraic logic programming: from Semantics to Implementation. J. Log. Comput. 26(2), 745–783 (2016)CrossRef
24.
Komendantskaya, E., Schmidt, M., Heras, J.: Exploiting parallelism in coalgebraic logic programming. Electr. Notes Theor. Comput. Sci. 303, 121–148 (2014)CrossRef
25.
26.
Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics. Springer, Heidelberg (1971)CrossRefMATH
27.
Power, A.J.: An algebraic formulation for data refinement. In: Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1989. LNCS, vol. 442, pp. 390–401. Springer, Heidelberg (1989)CrossRef
28.
Plotkin, G., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 1–24. Springer, Heidelberg (2001)CrossRef
29.
Plotkin, G., Power, J.: Notions of computation determine monads. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 342–356. Springer, Heidelberg (2002)CrossRef
30.
Simon, L., Bansal, A., Mallya, A., Gupta, G.: Co-logic programming: extending logic programming with coinduction. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 472–483. Springer, Heidelberg (2007)CrossRef
31.
Sterling, L., Shapiro, E.: The Art of Prolog. MIT Press, Cambridge (1986)MATH
32.
33.
Terese: Term Rewriting Systems. Cambridge University Press (2003)
34.
Worrell, J.: Terminal sequences for accessible endofunctors. In: Proceedings of the CMCS 1999. Electronic Notes in Theoretical Computer Science, vol. 19, pp. 24–38 (1999)
Metadata
Title
Category Theoretic Semantics for Theorem Proving in Logic Programming: Embracing the Laxness
Authors
Ekaterina Komendantskaya
John Power
Copyright Year
2016
Book
Coalgebraic Methods in Computer Science

Print ISBN: 978-3-319-40369-4

Electronic ISBN: 978-3-319-40370-0

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-40370-0_7

Premium Partner

    Image Credits