Abstract We study the recognition problem in the metaprogramming of finite normal predicate logic programs. That is, let $\mathcal{L}$ be a computable first-order predicate language with infinitely many constant symbols and infinitely many $n$-ary predicate symbols and $n$-ary functions symbols for all $n \geq 1$. Then we can effectively list all the finite normal predicate logic programs $Q_0,Q_1,\ldots $ over $\mathcal{L}$. Given some property $\mathcal{P}$ of finite normal predicate logic programs over $\mathcal{L}$, we define the index set $I_{\mathcal{P}}$ to be the set of indices $e$ such that $Q_e$ has property $\mathcal{P}$. We classify the complexity of the index set $I_{\mathcal{P}}$ within the arithmetic hierarchy for various natural properties of finite predicate logic programs. For example, we determine the complexity of the index sets relative to all finite predicate logic programs and relative to certain special classes of finite predicate logic programs of properties such as (i) having no stable models, (ii) having no recursive stable models, (iii) having at least one stable model, (iv) having at least one recursive stable model, (v) having exactly $c$ stable models for any given positive integer $c$, (vi) having exactly $c$ recursive stable models for any given positive integer $c$, (vii) having only finitely many stable models, (viii) having only finitely many recursive stable models, (ix) having infinitely many stable models and (x) having infinitely many recursive stable models.

A recent success of SAT solving has been the solution of the boolean Pythagorean Triples problem [Heule et al., 2016], delivering the largest proof yet, of 200 terabytes in size. We present this and the underlying paradigm Cube-and-Conquer, a powerful general method to solve big SAT problems, based on integrating the “old” and “new” methods of SAT solving.

The Cresco distributed agent-based framework is designed to address the challenges of edge computing. We present an actor-model implementation for the management of large numbers of geographically distributed services, comprised from heterogeneous resources and communication protocols, in support of low-latency realtime streaming applications. We present the purpose of our work, the basic methodology, the initial results already obtained, the relationship to the existing software, and the potential of the presently implemented framework to a number of potential further projects that could be developed on the basis of the existing implementation.

This paper accompanies panel contribution of the author to the session devoted to personal reminiscences of Professor Zdzisław Pawlak, a computer scientist and engineer.In particular we discuss some aspects of the work of Pawlak and researchers in his circle of collaborators in 1960ies, and especially, 1970ies.Given the lack of archival materials, the author bases this writing on personal recollections which may, at places, be imprecise.

The Constellation framework is designed for process automation, secure workload distribution, and performance optimization for genomic processing. The goal of Constellation is to provide a flexible platform for the processing of custom ”write once run anywhere” genomic pipelines, across a range of computational resources and environments, through the agent-based management of genomic processing containers. An implementation of the Constellation framework is currently in use at the University of Kentucky Medical Center for clinical diagnostic and research genomic processing.

Through the collection and association of discrete time-series resource metrics and workloads, we can both provide benchmark and intra-job resource collations, along with system-wide job profiling. Traditional RDBMSes are not designed to store and process long-term discrete time-series metrics and the commonly used resolution-reducing round robin databases (RRDB), make poor long-term sources of data for workload analytics. We implemented a system that employs “Big-data” (Hadoop/HBase) and other analytics (R) techniques and tools to store, process, and characterize HPC workloads. Using this system we have collected and processed over a 30 billion time-series metrics from existing short-term high-resolution (15-sec RRDB) sources, profiling over 200 thousand jobs across a wide spectrum of workloads. The system is currently in use at the University of Kentucky for better understanding of individual jobs and system-wide profiling as well as a strategic source of data for resource allocation and future acquisitions.

Answer Set Programming (ASP) is a logic programming, declarative, paradigm that was introduced in the late 1990s, based on the answer set semantics of logic programs proposed by Gelfond and Lifschitz a decade earlier.To date, ASP has been applied to a variety of domains and demonstrated its suitability for solving reasoning tasks such as knowledge-intensive tasks and combinatorial search problems.One direction of ASP research focuses on the development of efficient methods for computing answer sets.Novel techniques were initially adapted from SAT, then designed on purpose for ASP, e.g. to deal with specific ASP constructs, like aggregates, or to solve different reasoning tasks, such as cautious reasoning.More recently, ideas have been derived from the study of the relationship between ASP and other computing paradigms, such as constraint satisfaction, quantified Boolean formulas, first-order logic, pseudo-Boolean solvers, theorem provers, description logics, and external means of computation.The goal of this direction is to be able to cope more efficiently with practical problems, and to extend the domains that can be modeled and solved via ASP and its extensions.A recent, successful direction is CASP, which integrates ASP and constraint programming to solve problems with mixed discrete-continuous dynamics.The Answer Set Programming and Other Computing Paradigms (ASPOCP) series of workshops aims at fostering the cross-fertilization between ASP and other approaches by providing a venue for discussing advances in theory, solving techniques, and applications.Furthermore, the workshop encourages research that crosses the boundaries of ASP in other original directions, including action languages, probabilistic reasoning and machine learning, multi-agent and multi-context systems, argumentation frameworks and modularity.The ASPOCP workshop series has been held annually since its first edition in 2008 as a co-located event with the International Conference on Logic Programming (ICLP).The workshop has become an established event, as demonstrated by the considerable number of submissions and participants at each edition.The eighth edition of the workshop (ASPOCP 2015 1 ) was held in Cork, Ireland, on August 31st, 2015, as an affiliated event of the 31st ICLP meeting, which was part of "The Year of George Boole."Eleven papers were presented and the authors were invited to submit extended versions to be con-

All about Proofs, Proofs for All, Bruno Woltzenlogel Paleo and David Delahaye , Eds., College Publications, Series Mathematical Logic and Foundations, vol. 55., 2015. Paperback, ISBN 978-1-84890-166-7, vii + 240 pages. - Volume 16 Issue 2

Collections of network traces have long been used in network traffic analysis. Flow analysis can be used in network anomaly discovery, intrusion detection and more generally, discovery of actionable events on the network. The data collected during processing may be also used for prediction and avoidance of traffic congestion, network capacity planning, and the development of software-defined networking rules. As network flow rates increase and new network technologies are introduced on existing hardware platforms, many organizations find themselves either technically or financially unable to generate, collect, and/or analyze network flow data. The continued rapid growth of network trace data, requires new methods of scalable data collection and analysis. We report on our deployment of a system designed and implemented at the University of Kentucky that supports analysis of network traffic across the enterprise. Our system addresses problems of scale in existing systems, by using distributed computing methodologies, and is based on a combination of stream and batch processing techniques. In addition to collection, stream processing using Storm is utilized to enrich the data stream with ephemeral environment data. Enriched stream-data is then used for event detection and near real-time flow analysis by an in-line complex event processor. Batch processing is performed by the Hadoop MapReduce framework, from data stored in HBase BigTable storage.

Since 2004, the Mexican Logic and Computation Mexican Group, GMLogyC 1 has organized a number of meetings and workshops devoted to Logic and Computational Knowledge Representation.This initiative has been supported by a number of Mexican universities and research institutions.In particular GMLogyC organizes Latin American Workshop on Logic / Languages, Algorithms and New Methods of Reasoning (LANMR) a meeting of researchers in Computer Science Logic 2 .LANMR workshops have been international forums where the Latin American community interested in formal areas of Computer Science, meets together for presenting and discussing the research and development carried out all over the world.The objective of LANMR workshops is to bring together active Latin American researchers from different academic institutions who share a common interest in formal areas of Computer Science such as Computational Logic, formal languages, algorithms, and Knowledge Representation.Particular topics of interest are: logic programming and non-monotonic reasoning, logic-related algorithms, answer set programming, knowledge representation, belief representation, paraconsistent logics, deduction techniques, automated reasoning, reasoning about situations and actions, planning, preferences, default and abductive reasoning, argumentation, and other related topics.This issue of Fundamenta Informaticae contains extended and revised versions of papers selected from 13 papers that were presented at the Sixth edition of LANMR workshop.It is worth mentioning that we received 15 papers in LANMR 2010 and 13 of them were accepted.The list of these papers and details of the Program Committee are at the Volume 677 of CEUR Workshop Proceedings (seeThe selection process involved selecting the best seven papers from LANMR 2010, according to the original evaluations of the referees.Next, we invited the authors of these seven papers to present a journal version including proofs of results.

Abstract We investigate a proof system based on a guarded resolution rule and show its adequacy for the stable semantics of normal logic programs. As a consequence, we show that Gelfond–Lifschitz operator can be viewed as a proof-theoretic concept. As an application, we find a propositional theory EP whose models are precisely stable models of programs. We also find a class of propositional theories 𝓒P with the following properties. Propositional models of theories in 𝓒P are precisely stable models of P, and the theories in 𝓒T are of the size linear in the size of P.

Abstract We introduce and study logic programs whose clauses are built out ofmonotone constraint atoms. We show that the operational concept of the one-step provability operator generalizes to programs with monotone constraint atoms, but the generalization involves nondeterminism. Our main results demonstrate that our formalism is a common generalization of (1) normal logic programming with its semantics of models, supported models and stable models, (2) logic programming with weight atomslparseprograms) with the semantics of stable models, as defined by Niemelä, Simons and Soininen, and (3) of disjunctive logic programming with the possible-model semantics of Sakama and Inoue.

Abstract Logic programming requires that the programmer convert a problem into a set of constraints based on predicates. Choosing the predicates and introducing appropriate constraints can be intricate and error prone. If the problem domain is structured enough, we can let the programmer express the problem in terms of more abstract, higher‐level constraints. A compiler can then convert the higher‐level program into a logic‐programming formalism. The compiler writer can experiment with alternative low‐level representations of the higher‐level constraints in order to achieve a high‐quality translation. The programmer can then take advantage of both a reduction in complexity and an improvement in runtime speed for all problems within the domain. We apply this analysis to the domain of tabular constraint‐satisfaction problems. Examples of such problems include logic puzzles solvable on a hatch grid and combinatorial problems such as graph coloring and independent sets. The proper abstractions for these problems are rows, columns, entries, and their interactions. We present a higher‐level language, Constraint Lingo, dedicated to problems in this domain. We also describe how we translate programs from Constraint Lingo into lower‐level logic formalisms such as the logic of propositional schemata. These translations require that we choose among competing lower‐level representations in order to produce efficient results. The overall effectiveness of our approach depends on the appropriateness of Constraint Lingo, our ability to translate Constraint Lingo programs into high‐quality representations in logic formalisms, and the efficiency with which logic engines can compute answer sets. We comment on our computational experience with these tools in solving both graph problems and logic puzzles. Copyright © 2004 John Wiley & Sons, Ltd.

Schlipf (1995) proved that Stable Logic Programming (SLP) solves all decision problems. We extend Schlipf's result to prove that SLP solves all search problems in the class . Moreover, we do this in a uniform way as defined in Marek and Truszczyński (1991). Specifically, we show that there is a single program such that given any Turing machine with non-negative integer coefficients and any input , there is an extensional database such that there is a one-to-one correspondence between the stable models of $\mathit{edb}_{M,p,\sigma} \cup P_{\mathit{Trg}}$ and the accepting computations of the machine that reach the final state in at most steps. Moreover, can be computed in polynomial time from and the description of and the decoding of such accepting computations from its corresponding stable model of $\mathit{edb}_{M,p,\sigma} \cup P_{\mathit{Trg}}$ can be computed in linear time. A similar statement holds for Default Logic with respect to -search problems.The proof of this result involves additional technical complications and will be a subject of another publication.

In this paper constructions leading to the formation of belief sets by agents are studied. The focus is on the situation when possible belief sets are built incrementally in stages. An infinite sequence of theories that represents such a process is called a reasoning trace. A set of reasoning traces describing all possible reasoning scenarios for the agent is called a reasoning frame. Default logic by Reiter is not powerful enough to represent reasoning frames. In the paper a generalization of default logic of Reiter is introduced by allowing infinite sets of justifications. This formalism is called infinitary default logic. In the main result of the paper it is shown that every reasoning frame can be represented by an infinitary default theory. A similar representability result for antichains of theories (belief frames) is also presented.

Logic programming has been introduced as programming in the Horn clause subset of first-order logic. This view breaks down for the negation as failure inference rule. To overcome the problem, one line of research has been to view a logic program as a set of iff-definitions. A second approach was to identify a unique canonical, preferred , or intended model among the models of the program and to appeal to common sense to validate the choice of such model. Another line of research developed the view of logic programming as a nonmonotonic reasoning formalism strongly related to Default Logic and Autoepistemic Logic. These competing approaches have resulted in some confusion about the declarative meaning of logic programming. This paper investigates the problem and proposes an alternative epistemological foundation for the canonical model approach, which is not based on common sense but on a solid mathematical information principle. The thesis is developed that logic programming can be understood as a natural and general logic of inductive definitions . In particular, logic programs with negation represent nonmonotone inductive definitions . It is argued that this thesis results in an alternative justification of the well-founded model as the unique intended model of the logic program. In addition, it equips logic programs with an easy-to-comprehend meaning that corresponds very well with the intuitions of programmers.

We study properties of rough sets, that is, approximations to sets of records in a database or, more formally, to subsets of the universe of an information system. A rough set is a pair 〈L, U〉 such that L, U are definable in the information system and L ⊆ U. In the paper, we introduce a language, called the language of inclusion-exclusion, to describe incomplete specifications of (unknown) sets. We use rough sets in order to define a semantics for theories in the inclusion-exclusion language. We argue that our concept of a rough set is closely related to that introduced by Pawlak. We show that rough sets can be ordered by the knowledge ordering (denoted $\preceq$ kn )- We prove that Pawlak's rough sets are characterized as $\preceq$ kn -greatest approximations. We show that for any consistent (that is, satisfiable) theory T in the language of inclusion-exclusion there exists a $\preceq$ kn -greatest rough set approximating all sets X that satisfy T. For some classes of theories in the language of inclusion-exclusion, we provide algorithmic ways to find this best approximation. We also state a number of miscellaneous results and discuss some open problems.

Normal default logic, the fragment of default logic obtained by restricting defaults to rules of the form α:Mβ/β, is the most important and widely studied part of default logic. In [20], we proved a basis theorem for extensions of recursive propositi

In this paper we consider the complexity of the existence problem for explanations and for minimal explanations for abductive frameworks based on finite predicate programs. We find that although, in general, the problem is very complex, there are classes of frameworks for which the problem is much simpler.

It is wellknown that Minker's semantics GCWA for positive disjunctive programs P, i.e. to decide if a literal is true in all minimal models of P is ΠP2 -complete. This is in contrast to the same entailment problem for semantics of non-disjunctive pro

Normal default logic, the fragment of default logic obtained by restricting defaults to rules to the form /spl alpha/:M/spl beta///spl beta/. is the most important and widely studied part of default logic. In Annals of Pure and Applied Logic, vol. 67, pp. 269-324 (1994), we proved a basis theorem for extensions of recursive propositional logic normal default theories and hence for finite predicate logic normal default theories, i.e. we proved that every recursive propositional normal default theory possesses an extension which is recursively enumerable (r.e.) in 0'. In this paper, we show that this bound is tight. Specifically, we show that for every r.e. set A and every B which is r.e. in A, there is a recursive normal default theorywith a unique extension which is Turing-equivalent to A/spl oplus/B. A similar result holds for finite predicate logic normal default theories.

Many nonmonotonic formalism, including default logic, logic programming with stable models, and autoepistemic logic, can be represented faithfully by means of modal nonmonotonic logics in the family proposed by McDermott and Doyle. In this paper properties of logics in this family are thoroughly investigated. We present several results on characterization of expansions. These results are applicable to a wide class of nonmonotonic modal logics. Using these characterization results, algorithms for computing expansions for finite theories are developed. Perhaps the most important finding of this paper is that the structure of the family of modal nonmonotonic logics is much simpler than that of the family of underlying modal (monotonic) logics. Namely, it is often the case that different monotonic modal logics collapse to the same nonmonotonic system. We exhibit four families of logics whose nonmonotonic variants coincide: 5-KD45, TW5-SW5, N-WK , and W5-D4WB . These nonmonotonic logics naturally represent logics related to commonsense reasoning and knowledge representation such as autoepistemic logic, reflexive autoepistemic logic, default logic, and truth maintenance with negation.

In this paper we discuss the pure logic of necessitation N, a modal logic containing classical propositional calculus, with modus ponens and necessitation as inference rules, but without any axioms for manipulating modalities. We develop a theory of the logic N. We propose a sound and complete Kripke-like semantics for N and build a tableaux system for testing whether a formula is provable from a theory in the logic N. An alternative method to compute modal-free consequences of a finite theory is also given. Our main motivation to consider the logic N comes from the area of nonmonotonic reasoning. The nonmonotonic variant of N seems to be particularly useful in investigations of knowledge sets built when only partial information is available. In particular, this logic N is deeply connected with the default logic. In this paper, we apply our results to problems in nonmonotonic reasoning and we design algorithms for building the nonmonotonic consequence operator associated with N.

Autoepistemic logic is one of the principal modes of nonmonotonic reasoning. It unifies several other modes of nonmonotonic reasoning and has important application in logic programming. In the paper, a theory of autoepistemic logic is developed. This paper starts with a brief survey of some of the previously known results. Then, the nature of nonmonotonicity is studied by investigating how membership of autoepistemic statements in autoepistemic theories depends on the underlying objective theory. A notion similar to set-theoretic forcing is introduced. Expansions of autoepistemic theories are also investigated. Expansions serve as sets of consequences of an autoepistemic theory and they can also be used to define semantics for logic programs with negation. Theories that have expansions are characterized, and a normal form that allows the description of all expansions of a theory is introduced. Our results imply algorithms to determine whether a theory has a unique expansion. Sufficient conditions (stratification) that imply existence of a unique expansion are discussed. The definition of stratified theories is extended and (under some additional assumptions) efficient algorithms for testing whether a theory is stratified are proposed. The theorem characterizing expansions is applied to two classes of theories, K 1 -theories and ae-programs. In each case, simple hypergraph characterization of expansions of theories from each of these classes is given. Finally, connections with stable model semantics for logic programs with negation is discussed. In particular, it is proven that the problem of existence of stable models is NP-complete.— Authors' Abstract

The semantics for nonmonotonic rule systems are investigated. The notion of nonmonotonic formal systems is then introduced. Examples are given, along with applications of logic, logic programming, and common-sense reasoning.>

In various considerations of computer science (for instance in image processing and databases) one faces the following situation: Given a set (of points or of documents) one considers a descending sequence of equivalence relations (“approximation spaces of order Ξ”). These equivalence relations determine a sequence of closure operations Cli. Given a set X, the approximation sequence of X is simply i>ξ. We characterize here those sets X which satisfy the condition: X = ∩{Cli(X): i>Ξ}.

This paper contains some observations on models for A2-second-order arithmetics. It arose from unsuccessful attempts to prove the Conjecture 1 (see at the end of the paper). Two partial solutions are given in this paper. We also give a sketch of a new proof of a classical result of descriptive set-theory referred to in [3]. Unless otherwise specified the word “model” means “ω-model for second-order arithmetics with the axiom scheme of choice,” i.e., “ω-model of A2” in the terminology of [3]. We say that a model M1 is shorter than M2 iff there is in M2 a relation A which is a well-ordering in M2 such that every relation B which is a well-ordering in M1 is similar to an initial segment of A. We denote by M0 the principal model of A2, i.e., a model which has only standard integers and contains all sets of integers.