scholarly journals Verifying Tight Logic Programs with anthem and vampire

2020 ◽  
Vol 20 (5) ◽  
pp. 735-750
Author(s):  
JORGE FANDINNO ◽  
VLADIMIR LIFSCHITZ ◽  
PATRICK LÜHNE ◽  
TORSTEN SCHAUB
Keyword(s):  
Software Tools ◽  
Program Completion ◽  
Logic Programs ◽  
Input Language ◽  
First Order ◽  
Input And Output ◽  
Definition Of ◽  
Correctness Of Programs ◽  
The Relationship ◽  
Stable Models

AbstractThis paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas.

scholarly journals Lloyd-Topor completion and general stable models

2013 ◽  
Vol 13 (4-5) ◽  
pp. 503-515 ◽  
Author(s):  
VLADIMIR LIFSCHITZ ◽  
FANGKAI YANG
Keyword(s):  
Logic Program ◽  
Program Completion ◽  
Stable Model ◽  
First Order ◽  
The Relationship ◽  
Stable Models

AbstractWe investigate the relationship between the generalization of program completion defined in 1984 by Lloyd and Topor and the generalization of the stable model semantics introduced recently by Ferraris et al. The main theorem can be used to characterize, in some cases, the general stable models of a logic program by a first-order formula. The proof uses Truszczynski's stable model semantics of infinitary propositional formulas.

scholarly journals Temporal logic programs with variables

2016 ◽  
Vol 17 (2) ◽  
pp. 226-243 ◽  
Author(s):  
FELICIDAD AGUADO ◽  
PEDRO CABALAR ◽  
GILBERTO PÉREZ ◽  
CONCEPCIÓN VIDAL ◽  
MARTÍN DIÉGUEZ
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Logic Program ◽  
Answer Set Programming ◽  
Logic Programs ◽  
First Order ◽  
Linear Time Temporal Logic ◽  
Definition Of ◽  
Stable Models ◽  
Answer Set

AbstractIn this note, we consider the problem of introducing variables in temporal logic programs under the formalism of Temporal Equilibrium Logic, an extension of Answer Set Programming for dealing with linear-time modal operators. To this aim, we provide a definition of a first-order version of Temporal Equilibrium Logic that shares the syntax of first-order Linear-time Temporal Logic but has different semantics, selecting some Linear-time Temporal Logic models we call temporal stable models. Then, we consider a subclass of theories (called splittable temporal logic programs) that are close to usual logic programs but allowing a restricted use of temporal operators. In this setting, we provide a syntactic definition of safe variables that suffices to show the property of domain independence – that is, addition of arbitrary elements in the universe does not vary the set of temporal stable models. Finally, we present a method for computing the derivable facts by constructing a non-temporal logic program with variables that is fed to a standard Answer Set Programming grounder. The information provided by the grounder is then used to generate a subset of ground temporal rules which is equivalent to (and generally smaller than) the full program instantiation.

Program completion in the input language of GRINGO

2017 ◽  
Vol 17 (5-6) ◽  
pp. 855-871 ◽  
Author(s):  
AMELIA HARRISON ◽  
VLADIMIR LIFSCHITZ ◽  
DHANANJAY RAJU
Keyword(s):  
Reverse Engineering ◽  
Large Class ◽  
Logic Program ◽  
Answer Set Programming ◽  
Program Completion ◽  
Engineering Process ◽  
Input Language ◽  
Definition Of ◽  
Answer Set

AbstractWe argue that turning a logic program into a set of completed definitions can be sometimes thought of as the “reverse engineering” process of generating a set of conditions that could serve as a specification for it. Accordingly, it may be useful to define completion for a large class of Answer Set Programming (ASP) programs and to automate the process of generating and simplifying completion formulas. Examining the output produced by this kind of software may help programmers to see more clearly what their program does, and to what degree its behavior conforms with their expectations. As a step toward this goal, we propose here a definition of program completion for a large class of programs in the input language of the ASP grounder gringo, and study its properties.

scholarly journals Hyperbolicity of high-order systems of evolution equations

2015 ◽  
Vol 12 (01) ◽  
pp. 1-35 ◽  
Author(s):  
David Hilditch ◽  
Ronny Richter
Keyword(s):  
Evolution Equations ◽  
Arbitrary Order ◽  
Order Reduction ◽  
High Order ◽  
First Order ◽  
Definition Of ◽  
The Relationship

We study properties of evolution equations which are first order in time and arbitrary order in space (FTNS). Following Gundlach and Martín-García (2006) we define strong and symmetric hyperbolicity for FTNS systems and examine the relationship between these definitions, and the analogous concepts for first-order systems. We demonstrate equivalence of the FTNS definition of strong hyperbolicity with the existence of a strongly hyperbolic first-order reduction. We also demonstrate equivalence of the FTNS definition, up to N = 4, of symmetric hyperbolicity with the existence of a symmetric-hyperbolic first-order reduction.

Disjunctive logic programs with existential quantification in rule heads

2013 ◽  
Vol 13 (4-5) ◽  
pp. 563-578 ◽  
Author(s):  
JIA-HUAI YOU ◽  
HENG ZHANG ◽  
YAN ZHANG
Keyword(s):  
Stable Model ◽  
Logic Programs ◽  
Disjunctive Logic Programs ◽  
Decidable Fragment ◽  
Definition Of ◽  
Existential Quantification ◽  
Disjunctive Programs ◽  
Second Order Logic ◽  
Stable Models

AbstractWe consider disjunctive logic programs without function symbols but with existential quantification in rule heads, under the semantics of general stable models. There are at least two interesting prospects in these programs. The first is that a program can be made more succinct by using existential variables, and the second is on the potential in representing defeasible ontological knowledge by these logic programs. This paper studies some of the properties of these programs. First, we show a simple yet intuitive definition of stable models for these programs that does not resort to second-order logic. Second, the stable models of these programs can be characterized by an extension of progression for disjunctive programs, which provides a native characterization of justification for stable models. We then study the decidability issue. While the stable model existence problem for safe disjunctive programs is decidable, with existential quantification allowed in rule heads the problem becomes undecidable. We identify an interesting decidable fragment by exploring a new notion of stratification over existential quantification.

scholarly journals Stable models for infinitary formulas with extensional atoms

2016 ◽  
Vol 16 (5-6) ◽  
pp. 771-786
Author(s):  
AMELIA HARRISON ◽  
VLADIMIR LIFSCHITZ
Keyword(s):  
Programming Languages ◽  
Answer Set Programming ◽  
Splitting Theorem ◽  
First Order ◽  
Definition Of ◽  
Stable Models ◽  
Answer Set

AbstractThe definition of stable models for propositional formulas with infinite conjunctions and disjunctions can be used to describe the semantics of answer set programming languages. In this note, we enhance that definition by introducing a distinction between intensional and extensional atoms. The symmetric splitting theorem for first-order formulas is then extended to infinitary formulas and used to reason about infinitary definitions.

scholarly journals Relating Two Dialects of Answer Set Programming

2019 ◽  
Vol 19 (5-6) ◽  
pp. 1006-1020 ◽  
Author(s):  
AMELIA HARRISON ◽  
VLADIMIR LIFSCHITZ
Keyword(s):  
Working Group ◽  
Answer Set Programming ◽  
Stable Model ◽  
Input Language ◽  
Core Language ◽  
Definition Of ◽  
Stable Models ◽  
Answer Set

AbstractThe input language of the answer set solver clingo is based on the definition of a stable model proposed by Paolo Ferraris. The semantics of the ASP-Core language, developed by the ASP Standardization Working Group, uses the approach to stable models due to Wolfgang Faber, Nicola Leone, and Gerald Pfeifer. The two languages are based on different versions of the stable model semantics, and the ASP-Core document requires, “for the sake of an uncontroversial semantics,” that programs avoid the use of recursion through aggregates. In this paper we prove that the absence of recursion through aggregates does indeed guarantee the equivalence between the two versions of the stable model semantics, and show how that requirement can be relaxed without violating the equivalence property.

Nonlinear Analysis of Visual Evoked Potentials Elicited by Color Stimulation

1997 ◽  
Vol 36 (04/05) ◽  
pp. 315-318 ◽  
Author(s):  
K. Momose ◽  
K. Komiya ◽  
A. Uchiyama
Keyword(s):  
Visual System ◽  
Evoked Potentials ◽  
Visual Evoked Potentials ◽  
Normal Subjects ◽  
Second Order ◽  
First Order ◽  
The Relationship ◽  
Perceived Color ◽  
Second Order Nonlinearity ◽  
Visual Evoked

Abstract:The relationship between chromatically modulated stimuli and visual evoked potentials (VEPs) was considered. VEPs of normal subjects elicited by chromatically modulated stimuli were measured under several color adaptations, and their binary kernels were estimated. Up to the second-order, binary kernels obtained from VEPs were so characteristic that the VEP-chromatic modulation system showed second-order nonlinearity. First-order binary kernels depended on the color of the stimulus and adaptation, whereas second-order kernels showed almost no difference. This result indicates that the waveforms of first-order binary kernels reflect perceived color (hue). This supports the suggestion that kernels of VEPs include color responses, and could be used as a probe with which to examine the color visual system.

ADMINISTRATIVE AND LEGAL STATUS OF THE CAPITAL OF UKRAINE - THE HERO CITY OF KYIV AS A GUARANTEE OF THE RIGHTS OF CITIZENS OF UKRAINE AND THE TERRITORIAL COMMUNITY OF THE CITY

2017 ◽  
Author(s):  
Oleksii Chepov ◽  
Keyword(s):  
Legal Status ◽  
Modern World ◽  
Legal Regime ◽  
Legal Doctrine ◽  
City Councils ◽  
The Social ◽  
District Management ◽  
Definition Of ◽  
The Relationship ◽  
The City

The qualitative and clear definition of the legal regime of the capital of Ukraine, the hero city of Kyiv, is influenced by its legislative enshrinement, however, it should be noted that discussions are ongoing and one of the reasons for the unclear legal status of the capital is the ambiguity of current legislation in this area. Separation of the functions of the city of Kyiv, which are carried out to ensure the rights of citizens of Ukraine and the functions that guarantee the rights of the territorial community of the city of Kyiv. In the modern world, in legal doctrine and practice, the capital is understood as the capital of the country, which at the legislative level received this status and, accordingly, is the administrative and political center of the state, which houses the main state bodies and diplomatic missions of other states. It is the identification of the boundaries of the relationship between the competencies of state administrations and local self-government, in practice, often raises questions about their delimitation and ways of regulatory solution. Peculiarities of local self-government in Kyiv city districts are defined in the provisions of the Law on the Capital, which reveal the norms of the Constitution in these legal relations, according to which the issue of organizing district management in cities belongs to city councils. Likewise, it is unregulated by law to lose the particularity of the legal status of the territory of the city. It should be emphasized that the subject of administrative-legal relations is not a certain administrative-territorial entity, but the social group is designated - the territorial community of the city of Kiev, kiyani. Thus, the provisions on the city of Kyiv partially ignore the potential of the territorial community.

Compliance and Conflict of Value in Public Policy Implementation: Comparison between the New Order and the Reformation Era

2018 ◽  
Vol 2 (2) ◽  
pp. 99 ◽  
Author(s):  
Dwiyanto Indiahono ◽  
Erwan Purwanto ◽  
Agus Pramusinto
Keyword(s):  
Public Policy ◽  
Policy Implementation ◽  
Local Level ◽  
Group Discussion ◽  
New Order ◽  
The Reformation ◽  
Public Policy Implementation ◽  
Definition Of ◽  
Conflict Of Value ◽  
The Relationship

This research aims to examine differences in the relationship of bureaucratic and political officials during the New Order (Soeharto’s era) and the Reformation (post-Soeharto) era within the arena of public policy implementation. This is a matter of importance given that there is a change in relations between the two from integration in the New Order to bureaucratic impartiality in the Reformation Era. This study attempts to answer the question: How were the relations of bureaucratic and political officials in the implementation of local level public policy during the New Order and the Reformation Era? A qualitative research has been conducted in Tegal Municipality using the following data collection techniques: interview, focus group discussion, documentation, and observation. Tegal Municipality was selected as the study location because of the unique relationship shown between the mayor and the bureaucracy. Its uniqueness lies in the emergence of bureaucratic officials who dare to oppose political officials, based on their convictions that bureaucratic/public values should be maintained even if it means having to be in direct conflict with political officials. This research indicates that the relationship between bureaucratic and political officials in the arena of local level policy implementation during the New Order was characterized as being full of pressure and compliance, whereas during the Reformation Era bureaucrats have the audacity to hinder policy implementation. Such audacity to thwart policies is considered to have developed from a stance that aims to protect public budget and values in policies. The occurring conflict of values here demonstrates a dichotomy of political and bureaucratic officials that is different from the prevailing definition of politics-administration dichotomy introduced at the onset of Public Administration studies.

Sign in / Sign up

Export Citation Format

Share Document