×

Operational semantics of resolution and productivity in Horn clause logic. (English) Zbl 1362.68048


MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68N17 Logic programming
68N18 Functional programming and lambda calculus
68Q55 Semantics in the theory of computing

Software:

CoALP
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Arts T, Giesl J (2000) Termination of term rewriting using dependency pairs. Theor Comput Sci 236(12): 133-178 · Zbl 0938.68051 · doi:10.1016/S0304-3975(99)00207-8
[2] BarendregtHP (1992) Lambda calculiwith types. In:Abramsky S,GabbayD, Maibaum S (eds) Handbook of logic in computer science (vol. 2): background: computational structures. Oxford University Press, Inc., New York, pp 117-309
[3] Baader F, Nipkow T (1998) Term rewriting and all that. Cambridge University Press, New York · Zbl 0948.68098 · doi:10.1017/CBO9781139172752
[4] Fu P, Komendantskaya E, Schrijvers T, Pond A (2016) Proof relevant corecursive resolution. In: Functional and logic programming - 13th international symposium, FLOPS 2016, Kochi, Japan, 4-6 March 2016, proceedings, pp 126-143 · Zbl 1475.68054
[5] Gupta G, Bansal A, Min R, Simon L, Mallya A (2007) Coinductive logic programming and its applications. In: Logic programming, Springer, New York, pp 27-44 · Zbl 1213.68177
[6] Girard JY, Taylor P, Lafont Y (1989) Proofs and types. Cambridge University Press, New York · Zbl 0671.68002
[7] Harper R, Licata DR (2007) Mechanizing metatheory in a logical framework. J Funct Program 17(4-5): 613-673 · Zbl 1125.68029 · doi:10.1017/S0956796807006430
[8] Howard W (1980) The formulae-as-types notion of construction. In: Seldin J, Hindley J (eds), To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, Academic Press, New York, pp 479-490
[9] Jones SP, Jones M, Meijer E (1997) Type classes: an exploration of the design space. In: Haskell Workshop
[10] Johann P, Komendantskaya E, Komendantskiy V (2015) Structural resolution for logic programming. In Technical Communications, ICLP · Zbl 1407.68082
[11] Komendantskaya E, Johann P (2015) Structural resolution: a framework for coinductive proof search and proof construction in horn clause logic. In: ACM Transactions on Computational Logic, submitted
[12] Komendantskaya E, Johann P, Schmidt M (2016) A productivity checker for logic programming. On-line Pre-Proceedings of LOPSTR’16 “26th International Symposium on Logic-Based Program Synthesis and Transformation”, Edinburgh, UK. https://arxiv.org/abs/1608.02534 · Zbl 1485.68037
[13] Kleene SC (1980) Introduction to metamathematics, 8th edn. North-Holland Publishing Company, 1952. Co-publisher, Wolters-Noordhoff · Zbl 0047.00703
[14] Komendantskaya E, Power J (2011) Coalgebraic derivations in logic programming. In: CSL, pp 352-366 · Zbl 1247.68044
[15] Komendantskaya E, Power J, SchmidtM(2016) Coalgebraic logic programming: from semantics to implementation. J Logic Comput 26(2):745-783 · Zbl 1344.68044
[16] Lloyd JW (1987) Foundations of logic programming. Springer, New York · Zbl 0668.68004 · doi:10.1007/978-3-642-83189-8
[17] Lämmel R, Peyton-Jones S (2005) Scrap your boilerplate with class: Extensible generic functions. In: Proceedings of 10th ACM SIGPLAN international conference on functional programming, ICFP ’05, pp 204-215, New York, NY, USA, ACM · Zbl 1302.68062
[18] Miller D, Nadathur G, Pfenning F, Scedrov A (1991) Uniform proofs as a foundation for logic programming. Ann Pure Appl Logic 51(1-2):125-157 · Zbl 0721.03037
[19] Nilsson U, Małuszyński J (1990) Logic, programming and prolog. Wiley, Chichester · Zbl 0722.68023
[20] Pfenning F, Schürmann C (1999) System description: Twelfa meta-logical framework for deductive systems. In: Automated deduction CADE-16, pp 202-206, Springer, New York
[21] Simon L, Bansal A, Mallya A, Gupta G (2007) Co-logic programming: extending logic programming with coinduction. In: Automata, languages and programming, Springer, New York, pp 472-483 · Zbl 1171.68404
[22] Terese H (2003) Term rewriting systems. Cambridge University Press, Cambridge
[23] Zhou N-F, Fruhman J (2013) A user guide to Picat. Available from http://picat-lang.org. Accessed 15 Nov 2016
[24] Zhou N-F, Kjellerstrand H, Fruhman J (2015) Constraint solving and planning with picat. Springer, New York · doi:10.1007/978-3-319-25883-6
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.