status: Published

Abstract We address the problem of compiling defeasible theories to Datalog¬ programs. We prove the correctness of this compilation, for the defeasible logic DL(∂||), but the techniques we use apply to many other defeasible logics. Structural properties of DL(∂||) are identified that support efficient implementation and/or approximation of the conclusions of defeasible theories in the logic, compared with other defeasible logics. We also use previously well-studied structural properties of logic programs to adapt to incomplete Datalog¬ implementations.

The first issue of the journal Theory and Practice of Logic Programming, or TPLP, was published in January 2001.This issue, the last one in the present volume, and the following issue, the first one in the next volume, comprise a collection of papers commemorating and celebrating the twentieth anniversary of the journal.This celebratory collection comes with about one year delay due to the COVID-19 pandemic (but also, if we were to be entirely honest, because of a common human tendency to put things off).Whatever the true reason for the delay, the collection is finally here.We hope and expect it will prove to be a demonstration of the vitality of logic programming, and of a broad range of research directions it spawned in the past and continues to generate today.Logic programming appeared as a scientific subarea of computer science in the early 1970s as a result of the happy confluence of research on automated theorem proving in first-order logic and the original implementation of the Prolog programming language.The presence of these two original sources of inspiration has been distinctly felt over the years.On the one hand, logic programming attracted theoreticians pursuing deeper and highly nuanced understanding of the semantics of logic programs; on the other hand, it drew in researchers whose goal was to advance the repertoire of logic programming tools by refining, perfecting, and expanding Prolog, proposing and implementing new computational paradigms for logic programming, and developing methods to build and analyze logic programs.Moreover, and it also goes back to its very origins, logic programming attracted researchers interested in applications such as natural language processing, database querying, constraint solving, planning, learning, and knowledge representation, to name but a few.

Abstract In this note, we use Kunen’s notion of a signing to establish two theorems about the well-founded semantics of logic programs, in the case where we are interested in only (say) the positive literals of a predicate p that are consequences of the program. The first theorem identifies a class of programs for which the well-founded and Fitting semantics coincide for the positive part of p. The second theorem shows that if a program has a signing, then computing the positive part of p under the well-founded semantics requires the computation of only one part of each predicate. This theorem suggests an analysis for query answering under the well-founded semantics. In the process of proving these results, we use an alternative formulation of the well-founded semantics of logic programs, which might be of independent interest.

Abstract Recent technological advances have led to unprecedented amounts of generated data that originate from the Web, sensor networks, and social media. Analytics in terms of defeasible reasoning – for example, for decision making – could provide richer knowledge of the underlying domain. Traditionally, defeasible reasoning has focused on complex knowledge structures over small to medium amounts of data, but recent research efforts have attempted to parallelize the reasoning process over theories with large numbers of facts. Such work has shown that traditional defeasible logics come with overheads that limit scalability. In this work, we design a new logic for defeasible reasoning, thus ensuring scalability by design. We establish several properties of the logic, including its relation to existing defeasible logics. Our experimental results indicate that our approach is indeed scalable and defeasible reasoning can be applied to billions of facts.

There are a wide variety of formalisms for defeasible reasoning that can be seen as implementing concrete argumentation on defeasible rules. However there has been little work on the relationship between such languages and Dung’s abstract argumentation. In this paper we identify two small fragments of defeasible rule languages on which many concrete defeasible formalisms agree. The two fragments are closely related, as we show. Both arise as ways to express abstract argumentation frameworks in the concrete formalisms. Using these fragments, we establish a close relationship between abstract argumentation under semantics based on complete extensions, and ambiguity blocking logics in the framework of Antoniou et al. These results support a uniform approach to deriving complexity lower bounds for defeasible formalisms, where a lower bound is established for abstract argumentation and can then be extended “for free” to corresponding concrete defeasible formalisms.

Abstract Defeasible logics provide several linguistic features to support the expression of defeasible knowledge. There is also a wide variety of such logics, expressing different intuitions about defeasible reasoning. However, the logics can only combine in trivial ways. This limits their usefulness in contexts where different intuitions are at play in different aspects of a problem. In particular, in some legal settings, different actors have different burdens of proof, which might be expressed as reasoning in different defeasible logics. In this paper, we introduce annotated defeasible logic as a flexible formalism permitting multiple forms of defeasibility, and establish some properties of the formalism.

Abstract Open forms of global constraints allow the addition of new variables to an argument during the execution of a constraint program. Such forms are needed for difficult constraint programming problems, where problem construction and problem solving are interleaved, and fit naturally within constraint logic programming. However, in general, filtering that is sound for a global constraint can be unsound when the constraint is open. This paper provides a simple characterization, called contractibility, of the constraints, where filtering remains sound when the constraint is open. With this characterization, we can easily determine whether a constraint has this property or not. In the latter case, we can use it to derive a contractible approximation to the constraint. We demonstrate this work on both hard and soft constraints. In the process, we formulate two general classes of soft constraints.

Strategic argumentation provides a simple model of disputation. We investigate it in the context of Dung's abstract argumentation. We show that strategic argumentation under the grounded semantics is resistant tocorruption -- specifically, collusion and espionage — in a sense similar to Bartholdi et al's notion of a voting scheme resistant to manipulation. Under the stable semantics, strategic argumentation is resistant to espionage, but its resistance to collusion varies according to the aims of the disputants. These results are extended to a variety of concrete languages for argumentation.

In this paper we seek to formally establish the similarities and differences between two formalizations of defeasible reasoning: the defeasible logics of Nute and Maier, and defeasible logics in the framework of Antoniou et al. Both families of logics have developed from earlier logics of Nute, but their development has followed different paths and they are formulated very differently. We examine these logics from the standpoint of relative inference strength – how much the logics can infer from a given theory – and relative expressiveness – how well one logic can simulate another. We identify similarities between logics in the two families and pinpoint aspects that distinguish them.

Abstract Maher (2012) introduced an approach for relative expressiveness of defeasible logics, and two notions of relative expressiveness were investigated. Using the first of these definitions of relative expressiveness, we show that all the defeasible logics in the DL framework are equally expressive under this formulation of relative expressiveness. The second formulation of relative expressiveness is stronger than the first. However, we show that logics incorporating individual defeat are equally expressive as the corresponding logics with team defeat. Thus the only differences in expressiveness of logics in DL arise from differences in how ambiguity is handled. This completes the study of relative expressiveness in DL begun in Maher (2012).

Abstract We address the relative expressiveness of defeasible logics in the frameworkDL. Relative expressiveness is formulated as the ability to simulate the reasoning of one logic within another logic. We show that such simulations must be modular, in the sense that they also work if applied only to part of a theory, in order to achieve a useful notion of relative expressiveness. We present simulations showing that logics inDLwith and without the capability of team defeat are equally expressive. We also show that logics that handle ambiguity differently – ambiguity blocking versus ambiguity propagating – have distinct expressiveness, with neither able to simulate the other under a different formulation of expressiveness.

We consider the problem of network selection and flow distribution for a multihomed mobile device. We argue the benefits of a holistic approach which considers user- and application-centric metrics such as quality, energy consumption and monetary cost, rather than the commonly used network-centric metrics. We thus introduce the multihomed flow management problem which combines network selection, flow distribution and application flow awareness. We formulate it as a constrained optimisation problem and compare it to commonly used techniques: single network selection and load balancing. For selected interactive applications, we use empirical network measurements to evaluate the optimal solutions obtained by the three approaches. We show that, by exploiting the flexibility of application parameters, it is possible to achieve the potentially conflicting goals of maintaining high application quality while reducing both the power consumption and cost of network use.

Defeasible reasoning is a computationally simple nonmonotonic reasoning approach that has attracted significant theoretical and practical attention. It comprises a family of logics that capture different intuitions, among them ambiguity propagation versus ambiguity blocking, and the adoption or rejection of team defeat. This article provides a compact presentation of the defeasible logic variants, and derives an inclusion theorem which shows that different notions of provability in defeasible logic form a chain of levels of proof.

In recent years much research and implementation effort has been devoted both to multiparadigm languages and constraint programming languages. Following up on a series of 11 workshops (WFLP) on multiparadigm languages and constraint programming, and as a result of an open call for submissions, the journal on Theory and Practice of Logic Programming is now publishing the results of the selection of the papers submitted to this special issue.

Defeasible reasoning is a simple but efficient approach to nonmonotonic reasoning that has recently attracted considerable interest and that has found various applications. Defeasible logic and its variants are an important family of defeasible reasoning methods. So far no relationship has been established between defeasible logic and mainstream nonmonotonic reasoning approaches. In this paper we establish close links to known semantics of logic programs. In particular, we give a translation of a defeasible theory , instead.

In this paper we explore abduction over the Herbrand domain - equations on the algebra of finite terms (or finite trees) - which is a central element of logic programming and first-order automated reasoning. This paper is a case study of constraint abduction in the Herbrand domain. The direct relationship between Herbrand constraint abduction and type inference outlined above should make it easy to interpret the results of this paper in the context of type inference.

Defeasible reasoning is a simple but efficient rule-based approach to nonmonotonic reasoning. It has powerful implementations and shows promise to be applied in the areas of legal reasoning and the modelling of business rules. This paper establishes significant links between defeasible reasoning and argumentation. In particular, Dung-like argumentation semantics is provided for two key defeasible logics, of which one is ambiguity propagating and the other ambiguity blocking. There are several reasons for the significance of this work: (a) establishing links between formal systems leads to a better understanding and cross-fertilization, in particular our work sheds light on the argumentation-theoretic features of defeasible logic; (b) we provide the first ambiguity blocking Dung-like argumentation system; (c) defeasible reasoning may provide an efficient implementation platform for systems of argumentation; and (d) argumentation-based semantics support a deeper understanding of defeasible reasoning, especially in the context of the intended applications.

Local search techniques have attracted considerable interest in the artificial intelligence community since the development of GSAT and the min-conflicts heuristic for solving propositional satisfiability (SAT) problems and binary constraint satisfaction problems (CSPs) respectively. Newer techniques, such as the discrete Langrangian method (DLM), have significantly improved on GSAT and can also be applied to general constraint satisfaction and optimization. However, local search has yet to be successfully employed in solving temporal constraint satisfaction problems (TCSPs). This paper argues that current formalisms for representing TCSPs are inappropriate for a local search approach, and proposes an alternative CSP-based end-point ordering model for temporal reasoning. The paper looks at modelling and solving problems formulated using Allen's interval algebra (IA) and proposes a new constraint weighting algorithm derived from DLM. Using a set of randomly generated IA problems, it is shown that local search outperforms existing consistency-enforcing algorithms on those problems that the existing techniques find most difficult.

Local search techniques have attracted considerable interest in the artificial intelligence (AI) community since the development of GSAT (Selman et al., 1992) and the min-conflicts heuristic (Minton et al., 1992) for solving large propositional satisfiability (SAT) problems and binary constraint satisfaction problems (CSPs) respectively. Newer SAT techniques, such as the Discrete Langrangian Method (DLM) (Shang and Wah, 1998), have significantly improved on GSAT and can also be applied to general constraint satisfaction and optimisation. However, local search has yet to be successfully employed in solving temporal constraint satisfaction problems (TCSPs). We argue that current formalisms for representing TCSPs are inappropriate for a local search approach, and we propose an alternative CSP-based end-point ordering model for temporal reasoning. In particular we look at modelling and solving problems formulated using Allen's (1983) interval algebra (IA) and propose a new constraint weighting algorithm derived from DLM. Using a set of randomly generated IA problems, we show that our local search outperforms Nebel's (1997) backtracking algorithm on larger and more difficult consistent problems.

The importance of transformations and normal forms in logic programming, and generally in computer science, is well documented. This paper investigates transformations and normal forms in the context of Defeasible Logic, a simple but efficient formalism for nonmonotonic reasoning based on rules and priorities. The transformations described in this paper have two main benefits: on one hand they can be used as a theoretical tool that leads to a deeper understanding of the formalism, and on the other hand they have been used in the development of an efficient implementation of defeasible logic.

Defeasible logic is a rule-based nonmonotonic logic, with both strict and defeasible rules, and a priority relation on rules. We show that inference in the propositional form of the logic can be performed in linear time. This contrasts markedly with most other propositional nonmonotonic logics, in which inference is intractable.

For many years, the non-monotonic reasoning community has focussed on highly expressive logics. Such logics have turned out to be computationally expensive, and have given little support to the practical use of non-monotonic reasoning. In this work we discuss defeasible logic, a less-expressive but more efficient non-monotonic logic. We report on two new implemented systems for defeasible logic: a query answering system employing a backward chaining approach, and a forward-chaining implementation that computes all conclusions. Our experimental evaluation demonstrates that the systems can deal with large theories (up to hundreds of thousands of rules). We show that defeasible logic has linear complexity, which contrasts markedly with most other non-monotonic logics and helps to explain the impressive experimental results. We believe that defeasible logic, with its efficiency and simplicity is a good candidate to be used as a modelling language for practical applications, including modelling of regulations and business rules.

We investigate the implication problem for constrained tuple-generating dependencies (CTGDs), the extension of tuple- and equality-generating dependencies that permits expression of semantic relations (constraints) on variables. The implication problem is central to identifying redundant integrity constraints, checking integrity constraints on constraint databases, detecting independence of queries and updates, and optimizing queries. We provide two chase procedures for the implication problem. The first is cautious, generating tuples and constraints only when justified, whereas the second is speculative, generating tuples and constraints that have attached conditions about when they exist/hold. The cautious chase is more efficient, in some sense, but less powerful in demonstrating that a CTGD is implied. We demonstrate that, for constraint domains with Independence of Negative Constraints, the two chase procedures are equally powerful. The cautious chase is thus the chase of choice fo...

The filtering method considered in this paper is based on approximation of a spatial object in d-dimensional space by the minimal convex polyhedron that encloses the object and whose facets are normal to preselected axes. These axes are not necessarily the standard coordinate axes and, furthermore, their number is not determined by the dimension of the space. We optimize filtering by selecting optimal such axes based on a pre-processing analysis of stored objects or a sample thereof. The number of axes selected represents a trade-off between access time and storage overhead, as more axes usually lead to better filtering but require more overhead to store the associated access structures. We address the problem of minimizing the number of axes required to achieve a predefined quality of filtering and the reverse problem of optimizing the quality of filtering when the number of axes is fixed. In both cases we also show how to find an optimal collection of axes. In order to sol...

The problem of replaying computations of nondeterministic concurrent programs arises in contexts such as debugging and recovery. We investigate the problem for an abstract model of concurrency, which generalizes dataflow networks, processors with shared variables, and logic programming models of concurrency. We say that nondeterminism is visible if the state is determined, up to some (appropriately defined) notion of equivalence, by the external behavior. We show that if nondeterminism is visible then replay is achievable using a one-step lookahead sequential simulation algorithm. If the program has an additional monotonicity property called stability then recovery is possible without simulating the original computation, by restarting the program from a certain easily constructed state. Also, for stable programs with visible nondeterminism, a process composed of identical parallel processes has the same external behavior as each of its components. Hence high crash-failure res...

Complete axiomizations for the algebras of infinite trees and infinite trees are presented. The axiomizations are parameterized by the alphabet of function symbols for both the finite trees and infinite trees. There are two main cases, depending on whether the number of function symbols is finite or infinite. In the former case an extra axiom is necessary to obtain completeness. The method of proof is an elimination of quantifiers. Although a full elimination of quantifiers is not possible, the method forms the basis of decision procedures for the theories of the corresponding algebras. As a corollary to the results in infinite trees, the elementary equivalence of the algebra of rational trees and the algebra of infinite trees is obtained.>