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.

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.

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.

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

Answer Set Programming (ASP) is a declarative logic formalism that allows to encode computational problems via logic programs. Despite the declarative nature of the formalism, some advanced expertise is required, in general, for designing an ASP encoding that can be efficiently evaluated by an actual ASP system. A common way for trying to reduce the burden of manually tweaking an ASP program consists in automatically rewriting the input encoding according to suitable techniques, for producing alternative, yet semantically equivalent, ASP programs. However, rewriting does not always grant benefits in terms of performance; hence, proper means are needed for predicting their effects with this respect. In this paper we describe an approach based on Machine Learning (ML) to automatically decide whether to rewrite. In particular, given an ASP program and a set of input facts, our approach chooses whether and how to rewrite input rules based on a set of features measuring their structural properties and domain information. To this end, a Multilayer Perceptrons model has then been trained to guide the ASP grounder I-DLV on rewriting input rules. We report and discuss the results of an experimental evaluation over a prototypical implementation.

We propose an approach to the definition of microservices with an Answer Set Programming (ASP) `core', where microservices are a successful abstraction for designing distributed applications as suites of independently deployable interacting components. Such ASP-based components might be employed in distributed architectures related to Cloud Computing or to the Internet of Things (IoT).

We propose an epistemic approach to formalizing statistical properties of machine learning. Specifically, we introduce a formal model for supervised learning based on a Kripke model where each possible world corresponds to a possible dataset and modal operators are interpreted as transformation and testing on datasets. Then we formalize various notions of the classification performance, robustness, and fairness of statistical classifiers by using our extension of statistical epistemic logic (StatEL). In this formalization, we show relationships among properties of classifiers, and relevance between classification performance and robustness. As far as we know, this is the first work that uses epistemic models and logical formulas to express statistical properties of machine learning, and would be a starting point to develop theories of formal specification of machine learning.

Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are solicited in all areas of logic programming and related areas, including but not restricted to: - Foundations: Semantics, Formalisms, Answer-Set Programming, Non-monotonic Reasoning, Knowledge Representation. - Declarative Programming: Inference engines, Analysis, Type and mode inference, Partial evaluation, Abstract interpretation, Transformation, Validation, Verification, Debugging, Profiling, Testing, Logic-based domain-specific languages, constraint handling rules. - Related Paradigms and Synergies: Inductive and Co-inductive Logic Programming, Constraint Logic Programming, Interaction with SAT, SMT and CSP solvers, Logic programming techniques for type inference and theorem proving, Argumentation, Probabilistic Logic Programming, Relations to object-oriented and Functional programming, Description logics, Neural-Symbolic Machine Learning, Hybrid Deep Learning and Symbolic Reasoning. - Implementation: Concurrency and distribution, Objects, Coordination, Mobility, Virtual machines, Compilation, Higher Order, Type systems, Modules, Constraint handling rules, Meta-programming, Foreign interfaces, User interfaces. - Applications: Databases, Big Data, Data Integration and Federation, Software Engineering, Natural Language Processing, Web and Semantic Web, Agents, Artificial Intelligence, Bioinformatics, Education, Computational life sciences, Education, Cybersecurity, and Robotics.

Proof by induction is a long-standing challenge in Computer Science. Induction tactics of proof assistants facilitate proof by induction, but rely on humans to manually specify how to apply induction. In this paper, we present SeLFiE, a domain-specific language to encode experienced users' expertise on how to apply the induct tactic in Isabelle/HOL: when we apply an induction heuristic written in SeLFiE to an inductive problem and arguments to the induct tactic, the SeLFiE interpreter examines both the syntactic structure of the problem and semantics of the relevant constants to judge whether the arguments to the induct tactic are plausible according to the heuristic. Then, we present semantic_induct, an automatic tool to recommend how to apply the induct tactic. Given an inductive problem, semantic_induct produces candidate arguments to the induct tactic and selects promising ones using heuristics written in SeLFiE. Our evaluation based on 254 inductive problems from nine problem domains show that semantic_induct achieved 15.7 percentage points of improvements in coincidence rates for the three most promising recommendations while achieving 43% of reduction in the median value for the execution time when compared to an existing tool, smart_induct.

In this thesis we look into programming by example (PBE), which is about finding a program mapping given inputs to given outputs. PBE has traditionally seen a split between formal versus neural approaches, where formal approaches typically involve deductive techniques such as SAT solvers and types, while the neural approaches involve training on sample input-outputs with their corresponding program, typically using sequence-based machine learning techniques such as LSTMs [41]. As a result of this split, programming types had yet to be used in neural program synthesis techniques. We propose a way to incorporate programming types into a neural program synthesis approach for PBE. We introduce the Typed Neuro-Symbolic Program Synthesis (TNSPS) method based on this idea, and test it in the functional programming context to empirically verify type information may help improve generalization in neural synthesizers on limited-size datasets. Our TNSPS model builds upon the existing Neuro-Symbolic Program Synthesis (NSPS), a tree-based neural synthesizer combining info from input-output examples plus the current program, by further exposing information on types of those input-output examples, of the grammar production rules, as well as of the hole that we wish to expand in the program. We further explain how we generated a dataset within our domain, which uses a limited subset of Haskell as the synthesis language. Finally we discuss several topics of interest that may help take these ideas further. For reproducibility, we release our code publicly.