1,721,027 research outputs found
Andrea Formisano
No full textT -resolution parametrically generalizes standard resolution with respect to a first order theory T (the parameter). The inherent power of its derivation rule, however, makes it difficult to develop efficient unrestricted T -resolution based systems. CLP (X ) parametrically extends Horn clause logic programming with respect to a domain of computation X . The theory T underlying the domain X is fixed a-priori and cannot be modified (extended) by the user. In this paper we present the parametric logic programming language T logic programming (TLP) which extends the CLP -scheme by giving the possibility of acting on the theory T . The scheme is embedded into (linear) T -resolution; however, its syntax ensures that three rules (simple instances of the general T -resolution rule) are sufficient to implement the derivation process. Keywords: Theorem Proving, Constraint Logic Programming, Foundations. References ..
Extending and Implementing RASP
No full textIn previous work we have proposed an extension to ASP (Answer Set Programming), called RASP, standing for ASP with Resources. RASP supports declarative reasoning on production and consumption of (amounts of) resources. The approach combines answer set semantics with quantitative reasoning and relies on an algebraic structure to support computations and comparisons of amounts. The RASP framework provides some form of preference reasoning on resources usage. In this paper, we go further in this direction by introducing expressive constructs for supporting complex preferences specification on aggregate resources. We present a refinement of the semantics of RASP so as to take into account the new constructs. For all the extensions, we provide an encoding into plain ASP.We prove that the complexity of establishing the existence of an answer set, in such an enriched framework, remains NP-complete as in ASP. Finally, we report on raspberry, a prototypical implementation of RASP. This tool consists of a compiler that, given a ground RASP program, produces a pure ASP encoding suitable to be processed by commonly available ASP-solvers
ASPECT: Answer Set rePresentation as vEctor graphiCs in laTex
No full textLogic programming is a declarative programming paradigm that finds extensive use in the field of Artificial Intelligence (AI). As a result, it has become a valuable tool used in university courses for teaching students AI techniques. Besides Prolog language, the more recent Answer Set Programming (ASP) language turns out to be a powerful tool for developing advanced applications due to the expressiveness of the language and the availability of efficient solving systems. Unfortunately, the output of ASP solvers can be difficult to interpret, since it is a set of atoms, often long and verbose. This is most true in the case of students learning the language or in the case of experts developing applications for complex real-world problems. For these reasons, the ability to produce, when possible, a graphical representation of the solver output becomes useful to ensure easier interpretation of the results. In this paper we present ASPECT, a sub-language of ASP in which the user can directly define, in an intuitive and declarative way, a graphical representation of the answer set. The ASPECT atoms can be converted into the popular LaTeX markup language to produce vector graphics. The documents produced by ASPECT are easy to embed in documents such as scientific articles, course handouts, and presentations. Also, the development of user-friendly interfaces is critical for wider use of similar technologies in the industrial sector as well
Set-Based Invariants over Polynomial Systems
No full textDynamical systems model the time evolution of both natural and engineered processes. The automatic analysis of such models relies on different techniques ranging from reachability analysis, model checking, theorem proving, and abstractions. In this context, invariants are subsets of the state space containing all the states reachable from themself. The verification and synthesis of invariants is still a challenging problem over many classes of dynamical systems since it involves the analysis of an infinite time horizon. In this paper, we propose a method for computing invariants through sets of trajectories propagation. The method has been implemented and tested in the tool Sapo which provides reachability methods over discrete time polynomial dynamical systems
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Binary 3-compressible automata
No full textA finite deterministic automaton A = (Q, Σ, δ) is k-compressible if there is a word w ∈ Σ+ such that the image of the state
set Q under the natural action of w is reduced by at least k states. In such case w is called a k-compressing word for A. It is known that, for
any alphabet Σ and any k ≥ 2, there exist words that are k-compressing for each k-compressible automaton with the input alphabet Σ. Such
words are called k-collapsing. It has been proved that recognizing 2-collapsing words over a 2-element alphabet may be done in polynomial
time, while recognizing 2-collapsing words over an alphabet of size ≥ 3 is co-NP-complete. A natural question in this context, whether recognizing
3-collapsing words over a 2-element alphabet is easy or hard, has remained open. In this paper we provide results on 3-compressible binary
automata, which allow to prove that that the latter problem is co-NP-complet
Continued Hereditarily Finite Set-Approximations
Full text linkWe study an encoding RA that assigns a real number to each hereditarily finite set, in a broad sense. In particular, we investigate whether the map RA can be used to produce codes that approximate any positive real number α to arbitrary precision, in a way that is related to continued fractions. This is an interesting question because it connects the theory of hereditarily finite sets to the theory of real numbers and continued fractions, which have important applications in number theory, analysis, and other fields
- …
