| 1. |
- Busoniu, Paula-Andra, et al.
(författare)
-
SeaLion : An eclipse-based IDE for answer-set programming with advanced debugging support
- 2013
-
Ingår i: Theory and Practice of Logic Programming. - : Cambridge University Press. - 1471-0684 .- 1475-3081. ; 13:4-5, s. 657-673
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper, we present SeaLion, an integrated development environment (IDE) for answer-set programming (ASP). SeaLion provides source-code editors for the languages of Gringo and DLV and offers popular amenities like syntax highlighting, syntax checking, code completion, visual program outline, and refactoring functionality. The tool has been realised in the context of a research project whose goal is the development of techniques to support the practical coding process of answer-set programs. In this respect, SeaLion is the first IDE for ASP that provides debugging features that work for real-world answer-set programs and supports the rich languages of modern answer-set solvers. Indeed, SeaLion implements a stepping-based debugging approach that allows the developer to quickly track down programming errors by simply following his or her intuitions on the intended semantics. Besides that, SeaLion supports ASP development using model-driven engineering techniques including domain modelling with extended UML class diagrams and visualisation of answer sets in corresponding instance diagrams. Moreover, customised visualisation as well as visual editing of answer sets is realised by the Kara plugin of SeaLion. Further implemented features are a documentation generator based on the Lana annotation language, support for external solvers, and interoperability with external tools. SeaLion comes as a plugin of the popular Eclipse platform and provides interfaces for future extensions of the IDE.
|
|
| 2. |
- Cussens, James, et al.
(författare)
-
Introduction to the special issue on probability, logic and learning
- 2015
-
Ingår i: Theory and Practice of Logic Programming. - Cambridge : Cambridge University Press. - 1471-0684 .- 1475-3081. ; 15:2, s. 145-146
-
Tidskriftsartikel (refereegranskat)abstract
- Recently, the combination of probability, logic and learning has received considerable attention in the artificial intelligence and machine learning communities; see e.g. Getoor and Taskar (2007); De Raedt et al. (2008). Computational logic often plays a major role in these developments since it forms the theoretical backbone for much of the work in probabilistic programming and logical and relational learning. Contemporary work in this area is often application- and experiment-driven, but is also concerned with the theoretical foundations of formalisms and inference procedures and with advanced implementation technology that scales well.
|
|
| 3. |
- De Vos, Marina, et al.
(författare)
-
Annotating answer-set programs in Lana
- 2012
-
Ingår i: Theory and Practice of Logic Programming. - : Cambridge University Press. - 1471-0684 .- 1475-3081. ; 12:4-5, s. 619-637
-
Tidskriftsartikel (refereegranskat)abstract
- While past research in answer-set programming (ASP) mainly focused on theory, ASP solver technology, and applications, the present work situates itself in the context of a quite recent research trend: development support for ASP. In particular, we propose to augment answer-set programs with additional meta-information formulated in a dedicated annotation language, called Lana. This language allows the grouping of rules into coherent blocks and to specify language signatures, types, pre- and postconditions, as well as unit tests for such blocks. While these annotations are invisible to an ASP solver, as they take the form of program comments, they can be interpreted by tools for documentation, testing, and verification purposes, as well as to eliminate sources of common programming errors by realising syntax checking or code completion features. To demonstrate its versatility, we introduce two such tools, viz. (i) ASPDoc, for generating an HTML documentation for a program based on the annotated information, and (ii) ASPUnit, for running and monitoring unit tests on program blocks. Lana is also exploited in the SeaLion system, an integrated development environment for ASP based on Eclipse.
|
|
| 4. |
- Drabent, Wlodzimierz
(författare)
-
A simple correctness proof for magic transformation
- 2012
-
Ingår i: Theory and Practice of Logic Programming. - : Cambridge University Press (CUP). - 1471-0684 .- 1475-3081. ; 12:6, s. 929-936
-
Tidskriftsartikel (refereegranskat)abstract
- The paper presents a simple and concise proof of correctness of the magic transformation. We believe that it may provide a useful example of formal reasoning about logic programs. The correctness property concerns the declarative semantics. The proof, however, refers to the operational semantics (LD-resolution) of the source programs. Its conciseness is due to applying a suitable proof method.
|
|
| 5. |
- Drabent, Wlodzimierz
(författare)
-
Logic + control: On program construction and verification
- 2018
-
Ingår i: Theory and Practice of Logic Programming. - : Cambridge University Press. - 1471-0684 .- 1475-3081. ; 18:1, s. 1-29
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic program is constructed by means of stepwise refinement, hand in hand with its correctness and completeness proofs. The proofs are declarative – they do not refer to any operational semantics. Each step of the logic program construction follows a systematic approach to constructing programs which are provably correct and complete. We also prove that correctness and completeness of the logic program is preserved in the final Prolog program. Additionally, we prove termination, occur-check freedom and non-floundering.Our example shows how dealing with “logic” and with “control” can be separated. Most of the proofs can be done at the “logic” level, abstracting from any operational semantics.The example employs approximate specifications; they are crucial in simplifying reasoning about logic programs. It also shows that the paradigm of semantics-preserving program transformations may be not sufficient. We suggest considering transformations which preserve correctness and completeness with respect to an approximate specification.
|
|
| 6. |
- Drabent, Wlodzimierz, 1954-
(författare)
-
On Correctness and Completeness of an n Queens Program
- 2022
-
Ingår i: Theory and Practice of Logic Programming. - : Cambridge University Press. - 1471-0684 .- 1475-3081. ; 22:1, s. 37-50
-
Tidskriftsartikel (refereegranskat)abstract
- Thom Fruhwirth presented a short, elegant, and efficient Prolog program for the n queens problem. However, the program may be seen as rather tricky and one may not be convinced about its correctness. This paper explains the program in a declarative way and provides proofs of its correctness and completeness. The specification and the proofs are declarative, that is they abstract from any operational semantics. The specification is approximate, it is unnecessary to describe the programs semantics exactly. Despite the program works on non-ground terms, this work employs the standard semantics, based on logical consequence and Herbrand interpretations. Another purpose of the paper is to present an example of precise declarative reasoning about the semantics of a logic program.
|
|
| 7. |
- Drabent, Wlodzimierz
(författare)
-
On definite program answers and least Herbrand models
- 2016
-
Ingår i: Theory and Practice of Logic Programming. - : Cambridge University Press. - 1471-0684 .- 1475-3081. ; 16:4, s. 498-508
-
Tidskriftsartikel (refereegranskat)abstract
- A sufficient and necessary condition is given under which least Herbrand models exactlycharacterize the answers of definite clause programs.
|
|
| 8. |
- Drabent, Wlodzimierz, et al.
(författare)
-
Proving correctness and completeness of normal programs - A declarative approach
- 2005
-
Ingår i: Theory and Practice of Logic Programming. - 1471-0684 .- 1475-3081. ; 5:6, s. 669-711
-
Forskningsöversikt (refereegranskat)abstract
- We advocate a declarative approach to proving properties of logic programs. Total correctness can be separated into correctness, completeness and clean termination, the latter includes non-floundering. Only clean termination depends on the operational semantics, in particular on the selection rule. We show how to deal with correctness and completeness in a declarative way, treating programs only from the logical point of view. Specifications used in this approach are interpretations (or theories). We point out that specifications for correctness may differ from those for completeness, as usually there are answers which are neither considered erroneous nor required to be computed. We present proof methods for correctness and completeness for definite programs and generalize them to normal programs. For normal programs we use the 3-valued completion semantics, this is a standard semantics corresponding to negation as finite failure. The proof methods employ solely the classical 2-valued logic. We use a 2-valued characterization of the 3-valued completion semantics, which may be of separate interest. The method of proving correctness of definite programs is not new and can be traced back to the work of clark in 1979. However a more complicated approach using operational semantics was proposed by some authors. We show that it is not stronger than the declarative one, as far as properties of program answers are concerned. For a corresponding operational approach to normal programs, we show that it is (strictly) weaker than our method. We also employ the ideas of this work to generalize a known method of proving termination of normal programs. © 2005 Cambridge Univeristy Press.
|
|
| 9. |
- Drabent, Wlodzimierz, et al.
(författare)
-
Using parametric set constraints for locating errors in CLP programs
- 2002
-
Ingår i: Theory and Practice of Logic Programming. - 1471-0684 .- 1475-3081. ; 2:4-5, s. 549-610
-
Tidskriftsartikel (refereegranskat)abstract
- This paper introduces a framework of parametric descriptive directional types for Constraint Logic Programming (CLP). It proposes a method for locating type errors in CLP programs, and presents a prototype debugging tool. The main technique used is checking correctness of programs w.r.t. type specifications. The approach is based on a generalization of known methods for proving the correctness of logic programs to the case of parametric specifications. Set constraint techniques are used for formulating and checking verification conditions for (parametric) polymorphic type specifications. The specifications are expressed in a parametric extension of the formalism of term grammars. The soundness of the method is proved, and the prototype debugging tool supporting the proposed approach is illustrated on examples. The paper is a substantial extension of the previous work by the same authors concerning monomorphic directional types.
|
|
| 10. |
- Eiter, Thomas, et al.
(författare)
-
A Neuro-Symbolic ASP Pipeline for Visual Question Answering
- 2022
-
Ingår i: Theory and Practice of Logic Programming. - : Cambridge University Press. - 1471-0684 .- 1475-3081. ; 22:5, s. 739-754
-
Tidskriftsartikel (refereegranskat)abstract
- We present a neuro-symbolic visual question answering (VQA) pipeline for CLEVR, which is a well-known dataset that consists of pictures showing scenes with objects and questions related to them. Our pipeline covers (i) training neural networks for object classification and bounding-box prediction of the CLEVR scenes, (ii) statistical analysis on the distribution of prediction values of the neural networks to determine a threshold for high-confidence predictions, and (iii) a translation of CLEVR questions and network predictions that pass confidence thresholds into logic programmes so that we can compute the answers using an answer-set programming solver. By exploiting choice rules, we consider deterministic and non-deterministic scene encodings. Our experiments show that the non-deterministic scene encoding achieves good results even if the neural networks are trained rather poorly in comparison with the deterministic approach. This is important for building robust VQA systems if network predictions are less-than perfect. Furthermore, we show that restricting non-determinism to reasonable choices allows for more efficient implementations in comparison with related neuro-symbolic approaches without losing much accuracy.
|
|
