VERIFYING REQUIREMENTS THROUGH MATHEMATICAL MODELLING AND ANIMATION

2000 ◽  
Vol 10 (02) ◽  
pp. 251-273 ◽  
Author(s):  
EDMUND KAZMIERCZAK ◽  
PHILIP DART ◽  
LEON STERLING ◽  
MICHAEL WINIKOFF
Keyword(s):  
Mathematical Modelling ◽  
Operational Semantics ◽  
General Purpose ◽  
Automated Deduction ◽  
Mode Analysis ◽  
System Specification ◽  
Logic Programs ◽  
Requirements Specifications ◽  
Dependency Management ◽  
Semantics Of Logic Programs

Achieving confidence in the correctness, completeness and consistency of requirements specifications can be problematic and the consequences of incorrect requirements can be costly. In this paper we argue that specification and animation can provide reasonably high levels of assurance in the requirements without the overheads of using general purpose theorem proving tools. We propose a framework based on mode analysis and the operational semantics of logic programs for animating specifications. The framework allows us to combine prototyping and limited forms of automated deduction to increase our levels of confidence in specifications. Finally, we show how such a framework can be used to increase the level of confidence in the correctness of a simple dependency management system specification written in Z.

scholarly journals A Model-Theoretic Reconstruction of the Operational Semantics of Logic Programs

1993 ◽  
Vol 103 (1) ◽  
pp. 86-113 ◽  
Author(s):  
M. Falaschi ◽  
G. Levi ◽  
M. Martelli ◽  
C. Palamidessi
Keyword(s):  
Operational Semantics ◽  
Logic Programs ◽  
Semantics Of Logic Programs

TOPOLOGY AND THE SEMANTICS OF LOGIC PROGRAMS

1995 ◽  
Vol 24 (4) ◽  
pp. 359-386 ◽  
Author(s):  
Anthony Karel Seda
Keyword(s):  
Logic Programs ◽  
Semantics Of Logic Programs

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 Well-founded and stable semantics of logic programs with aggregates

2007 ◽  
Vol 7 (3) ◽  
pp. 301-353 ◽  
Author(s):  
NIKOLAY PELOV ◽  
MARC DENECKER ◽  
MAURICE BRUYNOOGHE
Keyword(s):  
Logic Programming ◽  
Second Order ◽  
Logic Programs ◽  
Consequence Operator ◽  
Trade Offs ◽  
Stable Semantics ◽  
Consequence Operators ◽  
Semantics Of Logic Programs ◽  
Stable Models

AbstractIn this paper, we present a framework for the semantics and the computation of aggregates in the context of logic programming. In our study, an aggregate can be an arbitrary interpreted second order predicate or function. We define extensions of the Kripke-Kleene, the well-founded and the stable semantics for aggregate programs. The semantics is based on the concept of a three-valuedimmediate consequence operatorof an aggregate program. Such an operatorapproximatesthe standard two-valued immediate consequence operator of the program, and induces a unique Kripke-Kleene model, a unique well-founded model and a collection of stable models. We study different ways of defining such operators and thus obtain a framework of semantics, offering different trade-offs betweenprecisionandtractability. In particular, we investigate conditions on the operator that guarantee that the computation of the three types of semantics remains on the same level as for logic programs without aggregates. Other results show that, in practice, even efficient three-valued immediate consequence operators which are very low in the precision hierarchy, still provide optimal precision.

scholarly journals Safe Inductions: An Algebraic Study

2017 ◽  
Author(s):  
Bart Bogaerts ◽  
Joost Vennekens ◽  
Marc Denecker
Keyword(s):  
Knowledge Representation ◽  
Logic Programming ◽  
Logic Programs ◽  
Intended Meaning ◽  
Safety Criterion ◽  
Autoepistemic Logic ◽  
Semantics Of Logic Programs ◽  
Do So

In many knowledge representation formalisms, a constructive semantics is defined based on sequential applications of rules or of a semantic operator. These constructions often share the property that rule applications must be delayed until it is safe to do so: until it is known that the condition that triggers the rule will remain to hold. This intuition occurs for instance in the well-founded semantics of logic programs and in autoepistemic logic. In this paper, we formally define the safety criterion algebraically. We study properties of so-called safe inductions and apply our theory to logic programming and autoepistemic logic. For the latter, we show that safe inductions manage to capture the intended meaning of a class of theories on which all classical constructive semantics fail.

Sign in / Sign up

Export Citation Format

Share Document