This paper presents a new type analysis for logic programs. The analysis is performed with a priori type definitions; and type expressions are formed from a fixed alphabet of type constructors. Non-discriminative union is used to join type information from different sources without loss of precision. An operation that is performed repeatedly during an analysis is to detect if a fixpoint has been reached. This is reduced to checking the emptiness of types. Due to the use of non-discriminative union, the fundamental problem of checking the emptiness of types is more complex in the proposed type analysis than in other type analyses with a priori type definitions. The experimental results, however, show that use of tabling reduces the effect to a small fraction of analysis time on a set of benchmarks.

Riveret et al. have proposed a framework for probabilistic legal reasoning. Their goal is to determine the chance of winning a court case, given the probabilities of the judge accepting certain claimed facts and legal rules.

In this paper we tackle the same problem by defining and implementing a new formalism, called probabilistic argumentation logic, which can be seen as a probabilistic generalization of Nute's defeasible logic. Not only does this provide an automation of the — only hand-performed — computations in Riveret et al, it also provides a solution to one of their open problems: a method to determine the initial probabilities from a given body of precedents.

Answer Set Programming (ASP) is a powerful form of declarative programming used in areas such as planning or reasoning. ASP solvers enforce stable model semantics, which rule out solutions representing certain kinds of circular reasoning. Unfortunately, current ASP solvers are incapable of solving problems involving cyclic dependencies between multiple integer or continuous quantities effectively. In this paper, we generalize the notion of stable models to bound founded variables with arbitrary domains, where bounds on such variables need to be justified by some rule in the program in order for the model to be stable. We show how to handle significantly more general rule forms where bound founded variables can act as head or body variables, and where head and body variables can be related via complex constraints subject to certain monotonicity requirements. We describe a new unfounded set detection algorithm which allows us to enforce this generalization of the stable model semantics. We also show how these unfounded sets can be explained in order to allow effective conflict-directed clause learning. The new solver merges the best features of CP, SAT and ASP solvers and allows new types of problems to be solved very efficiently.

In inductive learning of a broad concept, an algorithm should be able to distinguish concept examples from exceptions and noisy data. An approach through recursively finding patterns in exceptions turns out to correspond to the problem of learning default theories. Default logic is what humans employ in common-sense reasoning. Therefore, learned default theories are better understood by humans. In this paper, we present new algorithms to learn default theories in the form of non-monotonic logic programs. Experiments reported in this paper show that our algorithms are a significant improvement over traditional approaches based on inductive logic programming. Under consideration for acceptance in TPLP.

We present a new execution strategy for constraint logic programs called Failure Tabled CLP. Similarly to Tabled CLP our strategy records certain derivations in order to prune further derivations. However, our method only learns from failed derivations. This allows us to compute interpolants rather than constraint projection for generation of reuse conditions. As a result, our technique can be used where projection is too expensive or does not exist. Our experiments indicate that Failure Tabling can speed up the execution of programs with many redundant failed derivations as well as achieve termination in the presence of infinite executions.

We present a general approach to planning with incomplete information in Answer Set Programming (ASP). More precisely, we consider the problems of conformant and conditional planning with sensing actions and assumptions. We represent planning problems using a simple formalism where logic programs describe the transition function between states, the initial states and the goal states. For solving planning problems, we use Quantified Answer Set Programming (QASP), an extension of ASP with existential and universal quantifiers over atoms that is analogous to Quantified Boolean Formulas (QBFs). We define the language of quantified logic programs and use it to represent the solutions different variants of conformant and conditional planning. On the practical side, we present a translation-based QASP solver that converts quantified logic programs into QBFs and then executes a QBF solver, and we evaluate experimentally the approach on conformant and conditional planning benchmarks.

In this paper we consider Epistemic Logic Programs, which extend Answer Set Programming (ASP) with “ epistemic operators” and “ epistemic negation”, and a recent approach to the semantics of such programs in terms of World Views. We propose some observations on the existence and number of world views. We show how to exploit an extended ASP semantics in order to: (i) provide a characterization of world views, different from existing ones; (ii) query world views and query the whole set of world views.

This paper investigates how high school students in an introductory computer science (CS) course approach computing in the logic programming (LP) paradigm. This qualitative study shows how novice students operate within the LP paradigm while engaging in foundational computing concepts and skills: students are engaged in a cyclical process of abstraction, reasoning, and creating representations of their ideas in code while also being informed by the (procedural) requirements and the revision/debugging process. As these computing concepts and skills are also expected in traditional approaches to introductory K-12 CS courses, this paper asserts that LP is a viable paradigm choice for high school novices.

Decision support systems play an important role in medical fields as they can augment clinicians to deal more efficiently and effectively with complex decision-making processes. In the diagnosis of headache disorders, however, existing approaches and tools are still not optimal. On the one hand, to support the diagnosis of this complex and vast spectrum of disorders, the International Headache Society released in 1988 the International Classification of Headache Disorders (ICHD), now in its 3rd edition: a 200 pages document classifying more than 300 different kinds of headaches, where each is identified via a collection of specific nontrivial diagnostic criteria. On the other hand, the high number of headache disorders and their complex criteria make the medical history process inaccurate and not exhaustive both for clinicians and existing automatic tools. To fill this gap, we present head-asp, a novel decision support system for the diagnosis of headache disorders. Through a REST Web Service, head-asp implements a dynamic questionnaire that complies with ICHD-3 by exploiting two logical modules to reach a complete diagnosis while trying to minimize the total number of questions being posed to patients. Finally, head-asp is freely available on-line and it is receiving very positive feedback from the group of neurologists that is testing it.

Abstraction is a well-known approach to simplify a complex problem by over-approximating it with a deliberate loss of information. It was not considered so far in Answer Set Programming (ASP), a convenient tool for problem solving. We introduce a method to automatically abstract ASP programs that preserves their structure by reducing the vocabulary while ensuring an over-approximation (i.e., each original answer set maps to some abstract answer set). This allows for generating partial answer set candidates that can help with approximation of reasoning. Computing the abstract answer sets is intuitively easier due to a smaller search space, at the cost of encountering spurious answer sets. Faithful (non-spurious) abstractions may be used to represent projected answer sets and to guide solvers in answer set construction. For dealing with spurious answer sets, we employ an ASP debugging approach to help with abstraction refinement, which determines atoms as badly omitted and adds them back in the abstraction. As a show case, we apply abstraction to explain unsatisfiability of ASP programs in terms of blocker sets, which are the sets of atoms such that abstraction to them preserves unsatisfiability. Their usefulness is demonstrated by experimental results.

In this paper we address an issue that has been brought to the attention of the database community with the advent of the Semantic Web, i.e., the issue of how ontologies (and semantics conveyed by them) can help solving typical database problems, through a better understanding of Knowledge Representation (KR) aspects related to databases. In particular, we investigate this issue from the ILP perspective by considering two database problems, (i) the definition of views and (ii) the definition of constraints, for a database whose schema is represented also by means of an ontology. Both can be reformulated as ILP problems and can benefit from the expressive and deductive power of the KR framework . We illustrate the application scenarios by means of examples.

The Operating Room Scheduling (ORS) problem is the task of assigning patients to operating rooms (ORs), taking into account different specialties, lengths, and priority scores of each planned surgery, OR session durations, and the availability of beds for the entire length of stay (LOS) both in the Intensive Care Unit (ICU) and in the wards. A proper solution to the ORS problem is of primary importance for the healthcare service quality and the satisfaction of patients in hospital environments. In this paper we first present a solution to the problem based on Answer Set Programming (ASP). The solution is tested on benchmarks with realistic sizes and parameters, on three scenarios for the target length on 5-day scheduling, common in small–medium-sized hospitals, and results show that ASP is a suitable solving methodology for the ORS problem in such setting. Then, we also performed a scalability analysis on the schedule length up to 15 days, which still shows the suitability of our solution also on longer plan horizons. Moreover, we also present an ASP solution for the rescheduling problem, that is, when the offline schedule cannot be completed for some reason. Finally, we introduce a web framework for managing ORS problems via ASP that allows a user to insert the main parameters of the problem, solve a specific instance, and show results graphically in real time.

In this paper we take on Stuart C. Shapiro's challenge of solving the Jobs Puzzle automatically and do this via controlled natural language processing. Instead of encoding the puzzle in a formal language that might be difficult to use and understand, we employ a controlled natural language as a high-level specification language that adheres closely to the original notation of the puzzle and allows us to reconstruct the puzzle in a machine-processable way and add missing and implicit information to the problem description. We show how the resulting specification can be translated into an answer set program and be processed by a state-of-the-art answer set solver to find the solutions to the puzzle.

This paper formally compares some central notions from two well-known formalisms for rule-based argumentation, DeLP and ASPIC+. The comparisons especially focus on intuitive adequacy and inter-translatability, consistency, and closure properties. As for differences in the definitions of arguments and attack, it turns out that DeLP’s definitions are intuitively appealing but that they may not fully comply with Caminada and Amgoud’s rationality postulates of strict closure and indirect consistency. For some special cases, the DeLP definitions are shown to fare better than ASPIC+. Next, it is argued that there are reasons to consider a variant of DeLP with grounded semantics, since in some examples its current notion of warrant arguably has counterintuitive consequences and may lead to sets of warranted arguments that are not admissible. Finally, under some minimality and consistency assumptions on ASPIC+ arguments, a one-to-many correspondence between ASPIC+ arguments and DeLP arguments is identified in such a way that if the DeLP warranting procedure is changed to grounded semantics, then ’s DeLP notion of warrant and ASPIC+ ’s notion of justification are equivalent. This result is proven for three alternative definitions of attack.

Complex Event Recognition (CER) systems detect event occurrences in streaming time-stamped input using predefined event patterns. Logic-based approaches are of special interest in CER, since, via Statistical Relational AI, they combine uncertainty-resilient reasoning with time and change, with machine learning, thus alleviating the cost of manual event pattern authoring. We present a system based on Answer Set Programming (ASP), capable of probabilistic reasoning with complex event patterns in the form of weighted rules in the Event Calculus, whose structure and weights are learnt online. We compare our ASP-based implementation with a Markov Logic-based one and with a number of state-of-the-art batch learning algorithms on CER data sets for activity recognition, maritime surveillance and fleet management. Our results demonstrate the superiority of our novel approach, both in terms of efficiency and predictive performance. This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP).

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.

This paper introduces a formal definition of a Cyber-Physical System (CPS) in the spirit of the CPS Framework proposed by the National Institute of Standards and Technology (NIST). It shows that using this definition, various problems related to concerns in a CPS can be precisely formalized and implemented using Answer Set Programming (ASP). These include problems related to the dependency or conflicts between concerns, how to mitigate an issue, and what the most suitable mitigation strategy for a given issue would be. It then shows how ASP can be used to develop an implementation that addresses the aforementioned problems. The paper concludes with a discussion of the potentials of the proposed methodologies.

In functional logic programs, rules are applicable independently of textual order, i.e., any rule can potentially be used to evaluate an expression. This is similar to logic languages and contrary to functional languages, e.g., Haskell enforces a strict sequential interpretation of rules. However, in some situations it is convenient to express alternatives by means of compact default rules. Although default rules are often used in functional programs, the non-deterministic nature of functional logic programs does not allow to directly transfer this concept from functional to functional logic languages in a meaningful way. In this paper, we propose a new concept of default rules for Curry that supports a programming style similar to functional programming while preserving the core properties of functional logic programming, i.e., completeness, non-determinism, and logic-oriented use of functions. We discuss the basic concept and propose an implementation which exploits advanced features of functional logic languages.

We present verification methods for logic programs with delay declarations. The verified properties are termination and freedom from errors related to built-ins. Concerning termination, we present two approaches. The first approach tries to eliminate the well-known problem of speculative output bindings. The second approach is based on identifying the predicates for which the textual position of an atom using this predicate is irrelevant with respect to termination. Three features are distinctive of this work: it allows for predicates to be used in several modes; it shows that block declarations, which are a very simple delay construct, are sufficient to ensure the desired properties; it takes the selection rule into account, assuming it to be as in most Prolog implementations. The methods can be used to verify existing programs and assist in writing new programs.

We introduce an extended tableau calculus for answer set programming (ASP). Theproof system is based on the ASP tableaux defined in the work by Gebser andSchaub (Tableau calculi for answer set programming. In Proceedings ofthe 22nd International Conference on Logic Programming (ICLP 2006),S. Etalle and M. Truszczynski, Eds. Lecture Notes in Computer Science, vol.4079. Springer, 11–25) with an added extension rule. We investigatethe power of Extended ASP Tableaux both theoretically and empirically. We studythe relationship of Extended ASP Tableaux with the Extended Resolution proofsystem defined by Tseitin for sets of clauses, and separate Extended ASPTableaux from ASP Tableaux by giving a polynomial-length proof for a family ofnormal logic programs {Φn} for which ASP Tableaux has exponential-length minimal proofs withrespect to n. Additionally, Extended ASP Tableaux implyinteresting insight into the effect of program simplification on the lengths ofproofs in ASP. Closely related to Extended ASP Tableaux, we empiricallyinvestigate the effect of redundant rules on the efficiency of ASP solving.