scholarly journals On Correctness and Completeness of an n Queens Program

2021 ◽  
pp. 1-14
Author(s):  
WŁODZIMIERZ DRABENT
Keyword(s):  
Logical Consequence ◽  
Logic Program ◽  
Operational Semantics ◽  
Prolog Program ◽  
Declarative Reasoning

Abstract Thom Frühwirth presented a short, elegant, and efficient Prolog program for the n queens problem. However, the program may be seen as rather tricky and one may not be convinced about its correctness. This paper explains the program in a declarative way and provides proofs of its correctness and completeness. The specification and the proofs are declarative, that is they abstract from any operational semantics. The specification is approximate, it is unnecessary to describe the program’s semantics exactly. Despite the program works on non-ground terms, this work employs the standard semantics, based on logical consequence and Herbrand interpretations. Another purpose of the paper is to present an example of precise declarative reasoning about the semantics of a logic program.

scholarly journals Logic + control: On program construction and verification

2017 ◽  
Vol 18 (1) ◽  
pp. 1-29
Author(s):  
WŁODZIMIERZ DRABENT
Keyword(s):  
Logic Program ◽  
Practical Importance ◽  
Operational Semantics ◽  
Program Transformations ◽  
Logic Programs ◽  
Formal Reasoning ◽  
Prolog Program ◽  
Logic Control ◽  
Sat Solver ◽  
Program Construction

AbstractThis paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic program is constructed by means of stepwise refinement, hand in hand with its correctness and completeness proofs. The proofs are declarative – they do not refer to any operational semantics. Each step of the logic program construction follows a systematic approach to constructing programs which are provably correct and complete. We also prove that correctness and completeness of the logic program is preserved in the final Prolog program. Additionally, we prove termination, occur-check freedom and non-floundering.Our example shows how dealing with “logic” and with “control” can be separated. Most of the proofs can be done at the “logic” level, abstracting from any operational semantics.The example employs approximate specifications; they are crucial in simplifying reasoning about logic programs. It also shows that the paradigm of semantics-preserving program transformations may be not sufficient. We suggest considering transformations which preserve correctness and completeness with respect to an approximate specification.

scholarly journals Programming in logic without logic programming

2016 ◽  
Vol 16 (3) ◽  
pp. 269-295 ◽  
Author(s):  
ROBERT KOWALSKI ◽  
FARIBA SADRI
Keyword(s):  
Logic Programming ◽  
Logic Program ◽  
Operational Semantics ◽  
Canonical Model ◽  
State Transitions ◽  
Logic Programs ◽  
Initial State ◽  
State Sequence ◽  
Sequence Of Events ◽  
Current State

AbstractIn previous work, we proposed a logic-based framework in which computation is the execution of actions in an attempt to make reactive rules of the form if antecedent then consequent true in a canonical model of a logic program determined by an initial state, sequence of events, and the resulting sequence of subsequent states. In this model-theoretic semantics, reactive rules are the driving force, and logic programs play only a supporting role. In the canonical model, states, actions, and other events are represented with timestamps. But in the operational semantics (OS), for the sake of efficiency, timestamps are omitted and only the current state is maintained. State transitions are performed reactively by executing actions to make the consequents of rules true whenever the antecedents become true. This OS is sound, but incomplete. It cannot make reactive rules true by preventing their antecedents from becoming true, or by proactively making their consequents true before their antecedents become true. In this paper, we characterize the notion of reactive model, and prove that the OS can generate all and only such models. In order to focus on the main issues, we omit the logic programming component of the framework.

LOGIC PROGRAMMING AND DEFAULT LOGIC

1994 ◽  
Vol 03 (03) ◽  
pp. 367-373
Author(s):  
GRIGORIS ANTONIOU
Keyword(s):  
Logic Programming ◽  
Ad Hoc ◽  
Logic Program ◽  
Operational Semantics ◽  
Main Property ◽  
Default Logic ◽  
Logic Programs ◽  
Default Theory ◽  
Normal Logic ◽  
Direct Use

We present several ideas of increasing complexity how to translate default theories to normal logic programs that make direct use of the deductive capacity of logic programming. We show the limitations of simple, ad hoc approaches, and arrive at a more general construction; its main property is that the answer substitutions computed by the logic program via its standard operational semantics correspond exactly to the extensions of the default theory.

Stable and Supported Semantics in Continuous Vector Spaces

2020 ◽  
Author(s):  
Yaniv Aspis ◽  
Krysia Broda ◽  
Alessandra Russo ◽  
Jorge Lobo
Keyword(s):  
Logic Program ◽  
Matrix Multiplication ◽  
Vector Spaces ◽  
Continuous Space ◽  
Continuous Vector ◽  
Novel Approach ◽  
Gradient Based ◽  
Normal Logic ◽  
Parameter Values ◽  
Normal Logic Program

We introduce a novel approach for the computation of stable and supported models of normal logic programs in continuous vector spaces by a gradient-based search method. Specifically, the application of the immediate consequence operator of a program reduct can be computed in a vector space. To do this, Herbrand interpretations of a propositional program are embedded as 0-1 vectors in $\mathbb{R}^N$ and program reducts are represented as matrices in $\mathbb{R}^{N \times N}$. Using these representations we prove that the underlying semantics of a normal logic program is captured through matrix multiplication and a differentiable operation. As supported and stable models of a normal logic program can now be seen as fixed points in a continuous space, non-monotonic deduction can be performed using an optimisation process such as Newton's method. We report the results of several experiments using synthetically generated programs that demonstrate the feasibility of the approach and highlight how different parameter values can affect the behaviour of the system.

Glarner Waldwirtschaft im letzten Viertel des 20. Jahrhunderts | Glarner Forest Management in the last quarter of the 20th Century

2002 ◽  
Vol 153 (7) ◽  
pp. 249-250
Author(s):  
Fritz Marti
Keyword(s):  
Forest Management ◽  
20Th Century ◽  
Logical Consequence ◽  
Mountain Forest ◽  
Wood Production ◽  
Looking Back

Looking back on the last quarter of the 20th century, we see that the most striking changes in forest management have come about following large and frequent catastrophes. Management– concerned solely with wood production in former times – is oriented more towards retaining stability of the stands nowadays. In addition, the aspect of tending and improving the environment continues to gain ground. The growing gap between expenditure and profit is particularly acute in Glarner mountain forest areas. The extension of promotional silvicultural measures, which widely determines today's management, is to be seen as a logical consequence.

Essentialism and Logical Consequence

2018 ◽  
Author(s):  
Rosanna Keefe ◽  
Jessica Leech
Keyword(s):  
Logical Consequence ◽  
Prima Facie ◽  
Logical Pluralism ◽  
Logical Necessity ◽  
Popular View

According to an increasingly popular view, the source of logical necessity is to be found in the essences of logical entities. One might be tempted to extend the view further in using it to tackle fundamental questions surrounding logical consequence. This chapter enquires: how does a view according to which the facts about logical consequence are determined by the essences of logical entities look in detail? Are there any more or less obvious problems arising for such a view? The chapter uncovers a prima facie result in favour of logical pluralism. However, it then goes on to raise some concerns for this result. It argues that, considered generally, it is difficult to see how essence could do all of the requisite work alone. The chapter also shows how considering things from the perspective of disputes between particular rival logics makes an interesting and important difference to the picture of things presented by the essentialist account.

scholarly journals Specifying and Executing User Agents in an Environment of Reasoning and RESTful Systems Using the Guard-Stage-Milestone Approach

2021 ◽  
Author(s):  
Tobias Käfer ◽  
Benjamin Jochum ◽  
Nico Aßfalg ◽  
Leonard Nürnberg
Keyword(s):  
Linked Data ◽  
Operational Semantics ◽  
Workflow Management ◽  
Management Systems ◽  
Workflow Management Systems ◽  
The Web

AbstractFor Read-Write Linked Data, an environment of reasoning and RESTful interaction, we investigate the use of the Guard-Stage-Milestone approach for specifying and executing user agents. We present an ontology to specify user agents. Moreover, we give operational semantics to the ontology in a rule language that allows for executing user agents on Read-Write Linked Data. We evaluate our approach formally and regarding performance. Our work shows that despite different assumptions of this environment in contrast to the traditional environment of workflow management systems, the Guard-Stage-Milestone approach can be transferred and successfully applied on the web of Read-Write Linked Data.

scholarly journals Persistent Stochastic Non-Interference

2021 ◽  
Vol 181 (1) ◽  
pp. 1-35
Author(s):  
Jane Hillston ◽  
Andrea Marin ◽  
Carla Piazza ◽  
Sabina Rossi
Keyword(s):  
Process Algebra ◽  
Operational Semantics ◽  
Evaluation Process ◽  
Decision Algorithm ◽  
Secure Systems ◽  
Information Flow Security ◽  
Structural Operational Semantics ◽  
Timing Properties ◽  
Functional Point ◽  
Security Property

In this paper, we study an information flow security property for systems specified as terms of a quantitative Markovian process algebra, namely the Performance Evaluation Process Algebra (PEPA). We propose a quantitative extension of the Non-Interference property used to secure systems from the functional point view by assuming that the observers are able to measure also the timing properties of the system, e.g., the response time of certain actions or its throughput. We introduce the notion of Persistent Stochastic Non-Interference (PSNI) based on the idea that every state reachable by a process satisfies a basic Stochastic Non-Interference (SNI) property. The structural operational semantics of PEPA allows us to give two characterizations of PSNI: one based on a bisimulation-like equivalence relation inducing a lumping on the underlying Markov chain, and another one based on unwinding conditions which demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. A decision algorithm for PSNI is presented and an application of PSNI to a queueing system is discussed.

Sign in / Sign up

Export Citation Format

Share Document