On Completeness of Logic Programs

详细信息    查看全文

• 关键词：Logic programming ; Program completeness ; Declarative programming ; Approximate specification
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：8981
• 期：1
• 页码：261-278
• 全文大小：329 KB
• 参考文献：1.Apt, K.R.: From Logic Programming to Prolog. International Series in Computer Science. Prentice-Hall, Upper Saddle River (1997)
  2.Apt, K.R., Pedreschi, D.: Reasoning about termination of pure Prolog programs. Inf. Comput. 106(1), 109鈥?57 (1993)View Article MATH MathSciNet
  3.Bezem, M.: Strong termination of logic programs. J. Log. Program. 15(1&2), 79鈥?7 (1993)View Article MATH MathSciNet
  4.Clark, K.L.: Predicate logic as computational formalism. Technical report 79/59, Imperial College, London (1979)
  5. Deransart, P., Ma艂uszy艅ski, J.: A Grammatical View of Logic Programming. The MIT Press, Cambridge (1993) MATH
  6.Deville, Y.: Logic Programming: Systematic Program Development. Addison-Wesley, Reading (1990)
  7.Deville, Y., Lau, K.-K.: Logic program synthesis. J. Log. Program. 19(20), 321鈥?50 (1994)View Article MathSciNet
  8.Doets, K.: From Logic to Logic Programming. The MIT Press, Cambridge (1994)MATH
  9.Drabent, W.: Logic + control: an example. In: Dovier, A., Santos Costa, V. (eds.) Technical Communications of ICLP 2012. LIPIcs, vol. 17, pp. 301鈥?11 (2012). http://鈥媎rops.鈥媎agstuhl.鈥媎e/鈥媜pus/鈥媣olltexte/鈥?012/鈥?631
  10.Drabent, W.: Logic + control: an example of program construction, CoRR. abs/1110.4978 (2012). http://鈥媋rxiv.鈥媜rg/鈥媋bs/鈥?110.鈥?978.鈥?/span>
  11.Drabent, W.: Correctness and completeness of logic programs, CoRR. abs/1412.8739 (2014). http://鈥媋rxiv.鈥媜rg/鈥媋bs/鈥?412.鈥?739
  12.Drabent, W.: On completeness of logic programs, CoRR. abs/1411.3015(2014). http://鈥媋rxiv.鈥媜rg/鈥媋bs/鈥?411.鈥?015
  13.Drabent, W., Mi艂kowska, M.: Proving correctness and completeness of normal programs - a declarative approach. Theory Pract. Log. Program. 5(6), 669鈥?11 (2005)View Article MATH MathSciNet
  14.Genaim, S., King, A.: Inferring non-suspension conditions for logic programs with dynamic scheduling. ACM Trans. Comput. Log. 9(3), 17:1鈥?7:43 (2008)View Article MathSciNet
  15.Hogger, C.J.: Introduction to Logic Programming. Academic Press, London (1984)MATH
  16.Howe, J.M., King, A.: A pearl on SAT and SMT solving in Prolog. Theor. Comput. Sci. 435, 43鈥?5 (2012)View Article MATH MathSciNet
  17.King, A.: Personal communication, March 2012
  18.Kowalski, R.A.: The relation between logic programming and logic specification. In: Hoare, C., Shepherdson, J. (eds.) Mathematical Logic and Programming Languages, pp. 11鈥?7. Prentice-Hall, Upper Saddle River (1985). Also in Phil. Trans. R. Soc. Lond. A, 312, 345鈥?61(1984)
  19.Pettorossi, A., Proietti, M.: Transformation of logic programs: foundations and techniques. J. Log. Program. 19/20, 261鈥?20 (1994)View Article MathSciNet
  20. Pettorossi, A., Proietti, M., Senni, V.: The transformational approach to program development. In: Dovier, A., Pontelli, E. (eds.) GULP. LNCS, vol. 6125, pp. 112鈥?35. Springer, Heidelberg (2010) View Article
  21. Shapiro, E.: Algorithmic Program Debugging. The MIT Press, Cambridge (1983)
  22.St盲rk, R.F.: The theoretical foundations of LPTP (a logic program theorem prover). J. Log. Program. 36(3), 241鈥?69 (1998)View Article MATH
  23. Sterling, L., Shapiro, E.: The Art of Prolog, 2nd edn. The MIT Press, Cambridge (1994) MATH
  
• 作者单位：W艂odzimierz Drabent (15)
  
  15. Institute of Computer Science, Polish Academy of Sciences and IDA, Link枚pings Universitet, Link枚ping, Sweden
  
• 丛书名：Logic-Based Program Synthesis and Transformation
• ISBN：978-3-319-17822-6
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

Program correctness (in imperative and functional programming) splits in logic programming into correctness and completeness. Completeness means that a program produces all the answers required by its specification. Little work has been devoted to reasoning about completeness. This paper presents a few sufficient conditions for completeness of definite programs. We also study preserving completeness under some cases of pruning of SLD-trees (e.g. due to using the cut). We treat logic programming as a declarative paradigm, abstracting from any operational semantics as far as possible. We argue that the proposed methods are simple enough to be applied, possibly at an informal level, in practical Prolog programming. We point out importance of approximate specifications.