Goto

Collaborating Authors

 Logic & Formal Reasoning


SQuARE: Semantics-based Question Answering and Reasoning Engine

arXiv.org Artificial Intelligence

Understanding the meaning of a text is a fundamental challenge of natural language understanding (NLU) and from its early days, it has received significant attention through question answering (QA) tasks. We introduce a general semantics-based framework for natural language QA and also describe the SQuARE system, an application of this framework. The framework is based on the denotational semantics approach widely used in programming language research. In our framework, valuation function maps syntax tree of the text to its commonsense meaning represented using basic knowledge primitives (the semantic algebra) coded using answer set programming (ASP). We illustrate an application of this framework by using VerbNet primitives as our semantic algebra and a novel algorithm based on partial tree matching that generates an answer set program that represents the knowledge in the text. A question posed against that text is converted into an ASP query using the same framework and executed using the s(CASP) goal-directed ASP system. Our approach is based purely on (commonsense) reasoning. SQuARE achieves 100% accuracy on all the five datasets of bAbI QA tasks that we have tested. The significance of our work is that, unlike other machine learning based approaches, ours is based on "understanding" the text and does not require any training. SQuARE can also generate an explanation for an answer while maintaining high accuracy.


Tabling Optimization for Contextual Abduction

arXiv.org Artificial Intelligence

The requirement for artificial intelligence (AI) to provide explanations in making critical decision becomes increasingly important due to concerns of accountability, trust, as well as ethics. Such an explainable AI is expected to be capable of providing justifications that are human-understandable. A form of reasoning for providing explanations to an observation, known as abduction, has been well studied in AI, particularly in knowledge representation and reasoning. It extends to logic programming, dubbed abductive logic programming [3], and it has a wide variety of usage, e.g., in planning, scheduling, reasoning of rational agents, security protocols verification, biological systems, and machine ethics.


Automated Aggregator -- Rewriting with the Counting Aggregate

arXiv.org Artificial Intelligence

Answer set programming is a leading declarative constraint programming paradigm with wide use for complex knowledge-intensive applications. Modern answer set programming languages support many equivalent ways to model constraints and specifications in a program. However, so far answer set programming has failed to develop systematic methodologies for building representations that would uniformly lend well to automated processing. This suggests that encoding selection, in the same way as algorithm selection and portfolio solving, may be a viable direction for improving performance of answer-set solving. The necessary precondition is automating the process of generating possible alternative encodings. Here we present an automated rewriting system, the Automated Aggregator or AAgg, that given a non-ground logic program, produces a family of equivalent programs with complementary performance when run under modern answer set programming solvers. We demonstrate this behavior through experimental analysis and propose the system's use in automated answer set programming solver selection tools.


Splitting a Hybrid ASP Program

arXiv.org Artificial Intelligence

Hybrid Answer Set Programming (Hybrid ASP) is an extension of Answer Set Programming (ASP) that allows ASPlike rules to interact with outside sources. The Splitting Set Theorem is an important and extensively used result for ASP. The paper introduces the Splitting Set Theorem for Hybrid ASP, which is for Hybrid ASP the equivalent of the Splitting Set Theorem, and shows how it can be applied to simplify computing answer sets for Hybrid ASP programs most relevant for practical applications. An important result for logic programs is the Splitting Set Theorem [12], which shows how computing an answer set for a program can be broken into several tasks of the same kind for smaller programs. The theorem and its more general variant the Splitting Sequence Theorem are extensively used for proving other theorems, for instance in [1], [9] or [3] among many others. Hybrid Answer Set Programming (Hybrid ASP) [4] is an extension of ASP that allows ASPlike rules to interact with outside sources, which makes Hybrid ASP well suited for practical applications.


Dynamic Multi-Agent Path Finding based on Conflict Resolution using Answer Set Programming

arXiv.org Artificial Intelligence

We study a dynamic version of multi-agent path finding problem (called D-MAPF) where existing agents may leave and new agents may join the team at different times. We introduce a new method to solve D-MAPF based on conflict-resolution. The idea is, when a set of new agents joins the team and there are conflicts, instead of replanning for the whole team, to replan only for a minimal subset of agents whose plans conflict with each other. We utilize answer set programming as part of our method for planning, replanning and identifying minimal set of conflicts.


Logic Programming and Machine Ethics

arXiv.org Artificial Intelligence

Autonomous Intelligent Systems are designed to reduce the need for human intervention in our daily life. However, the full benefit of these new systems will be attained only if they are aligned with society's values and ethical principles. Adopting ethical approaches to building such systems has been attracting a lot of attention in the recent years. The global concern about the ethical behavior of this kind of technologies has manifested in many initiatives at different levels. As examples, we mention: the IEEE initiative for ethically aligned design of autonomous intelligent systems ('Ethics in Action'


Sequent-Type Calculi for Systems of Nonmonotonic Paraconsistent Logics

arXiv.org Artificial Intelligence

Paraconsistent logics constitute an important class of formalisms dealing with non-trivial reasoning from inconsistent premisses. In this paper, we introduce uniform axiomatisations for a family of nonmonotonic paraconsistent logics based on minimal inconsistency in terms of sequent-type proof systems. The latter are prominent and widely-used forms of calculi well-suited for analysing proof search. In particular, we provide sequent-type calculi for Priest's three-valued minimally inconsistent logic of paradox, and for four-valued paraconsistent inference relations due to Arieli and Avron. Our calculi follow the sequent method first introduced in the context of nonmonotonic reasoning by Bonatti and Olivetti, whose distinguishing feature is the use of a so-called rejection calculus for axiomatising invalid formulas. In fact, we present a general method to obtain sequent systems for any many-valued logic based on minimal inconsistency, yielding the calculi for the logics of Priest and of Arieli and Avron as special instances.


LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories

arXiv.org Artificial Intelligence

Answer set programming (ASP) is a well-established knowledge representation formalism that grew from the observation that stable models [33] of a logic program can be used to encode search problems [59, 62, 49]. ASP is rapidly gaining adoption, with applications in domains such as decision support for the Space Shuttle [63], product configuration [75], phylogenetic inference [45, 11], knowledge management [37], e-Tourism [65], biology [32], robotics [5], and machine learning [41, 12]. The success of ASP can, to a large extend, be explained by two factors. The first factor is a rich, first-order language, ASP-Core2 [13], to express knowledge in, with an easy-to-understand modeling methodology known as generate-define-and-test. The second factor is the availability of a large number of reliable tools -- grounders [31, 46] and solvers [28, 3, 16] -- that allow to efficiently compute stable models of a given logic program. Throughout its history, ASP has always benefited from progress in other domains of combinatorial search. For instance, the addition of conflict-driven clause learning (CDCL) [60] to Boolean satisfiability (SAT) solvers is often recognized as one of the most important leaps forward in SAT solving; this technique was very quickly adopted in ASP.


A System for Explainable Answer Set Programming

arXiv.org Artificial Intelligence

Answer Set Programming (ASP) [13, 12, 4] is a successful paradigm for Knowledge Representation and problem solving. Under this paradigm, the programmer represents a problem as a logic program formed by a set of rules and obtains solutions to that problem in terms of models of the program called answer sets. Thanks to the availability of efficient solvers, ASP is nowadays applied in a wide variety of areas including robotics, bioinformatics, music composition [7, 5, 3], and many more. An ASP program does not contain information about the method to obtain the answer sets, something that is completely delegated to the ASP solver. This, of course, has the advantage of making ASP a fully declarative language, where the programmer must concentrate on specification rather than on design of search algorithms.


Logical Judges Challenge Human Judges on the Strange Case of B.C.-Valjean

arXiv.org Artificial Intelligence

The connections between logic programming and law have been studied for a long time. In 1975, Meldman discussed his PhD Thesis entitled "A preliminary study in computer-aided legal analysis" [12] where he modelled legal facts in a Lisp-like language and used instantiation (recalling unification) and syllogism (recalling resolution) to perform a simple kind of legal analysis inspired by Prosser's Law of Torts [13]. At that time Prolog was just born, but its applications to legal reasoning were not long in coming. One of the first attempts was made by Hustler [9] who implemented a prototype of a legal consultant in Prolog, again inspired by Prosser's work. A few years later, Kowalski, Sergot et al. succeeded in running a significant portion of the 1981 British Nationality Act, implemented in Prolog on a small micro computer [15]. In the same years, Prolog became very popular for implementing expert systems for the legal domain [3, 19]. From those early attempts, much progress has been made: research on deontic and defeasible reasoning [1, 5], ontological reasoning [7], and argumentation [8, 18] is extremely lively and helps disclosing the many connections between logic programming (and, more in general, computational logic and automated reasoning) and legal reasoning. The application of automated reasoning to digital forensics is another promising research direction [6] whose potential is witnessed by the ongoing "Digital Forensics: Evidence Analysis via Intelligent Systems and Practices" (DigForASP) COST Action