Algorithmic Logic with Recursive Functions

1981 ◽  
Vol 4 (4) ◽  
pp. 975-995
Author(s):  
Andrzej Szałas
Keyword(s):  
Completeness Theorem ◽  
Inference Rules ◽  
Partial Correctness ◽  
Recursive Functions ◽  
Algorithmic Logic ◽  
Block Structured

A language is considered in which the reader can express such properties of block-structured programs with recursive functions as correctness and partial correctness. The semantics of this language is fully described by a set of schemes of axioms and inference rules. The completeness theorem and the soundness theorem for this axiomatization are proved.

PAL – Propositional Algorithmic Logic

1981 ◽  
Vol 4 (3) ◽  
pp. 675-760
Author(s):  
Grażyna Mirkowska
Keyword(s):  
Data Structures ◽  
Completeness Theorem ◽  
Natural Numbers ◽  
First Order ◽  
Algorithmic Logic ◽  
Axiomatic Systems ◽  
Nondeterministic Program ◽  
Basic Sets

The aim of propositional algorithmic logic is to investigate the properties of program connectives. Complete axiomatic systems for deterministic as well as for nondeterministic interpretations of program variables are presented. They constitute basic sets of tools useful in the practice of proving the properties of program schemes. Propositional theories of data structures, e.g. the arithmetic of natural numbers and stacks, are constructed. This shows that in many aspects PAL is close to first-order algorithmic logic. Tautologies of PAL become tautologies of algorithmic logic after replacing program variables by programs and propositional variables by formulas. Another corollary to the completeness theorem asserts that it is possible to eliminate nondeterministic program variables and replace them by schemes with deterministic atoms.

How powerful are folding/unfolding transformations?

1994 ◽  
Vol 4 (1) ◽  
pp. 89-112 ◽  
Author(s):  
Hong Zhu
Keyword(s):  
Necessary Condition ◽  
Efficiency Gain ◽  
Partial Correctness ◽  
Recursive Functions

AbstractThis paper discusses the transformation power of Burstall and Darlington's folding/unfolding system, i.e. what kind of programs can be derived from a given one. A necessary condition of derivability is proved. The notion of inherent complexity of recursive functions in introduced. A bound on efficiency gain by folding/unfolding transformations is obtained for all reasonable computation models. The well-known partial correctness and incompleteness of the system are corollaries of the result. Examples of underivability are given, e.g. binary searching cannot be derived from linear searching, merge sorting cannot be derived from insert sorting.

Effectivity problems of algorithmic logic

1977 ◽  
Vol 1 (1) ◽  
pp. 19-32
Author(s):  
Antoni Kreczmar
Keyword(s):  
Weak Equivalence ◽  
Basic Tool ◽  
Halting Problem ◽  
Partial Correctness ◽  
Algorithmic Logic

In the paper we solve some effectivity problems of program schemas. Such properties of programs as, for example, the strong and the weak equivalence, the correctness and the partial correctness of a program, the halting problem are classified in Kleene-Mostowski hierarchy. A basic tool used in the paper is algorithmic logic.

scholarly journals Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System

2021 ◽  
Vol 28 (4) ◽  
pp. 372-393
Author(s):  
Dmitry A. Kondratyev
Keyword(s):  
Automatic Parallelization ◽  
Parallel Execution ◽  
Programming System ◽  
Inference Rules ◽  
Deductive Verification ◽  
Recursive Functions ◽  
Axiomatic Semantics ◽  
Verification Conditions ◽  
Symbolic Method ◽  
Verification Condition

The C-lightVer system is developed in IIS SB RAS for C-program deductive verification. C-kernel is an intermediate verification language in this system. Cloud parallel programming system (CPPS) is also developed in IIS SB RAS. Cloud Sisal is an input language of CPPS. The main feature of CPPS is implicit parallel execution based on automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is automatic parallelization of such a superset of C that allows implementing automatic verification. Our solution is such a superset of C-kernel as C-Sisal-kernel. The first result presented in this paper is an extension of C-kernel by Cloud-Sisal-kernel loops. We have obtained the C-Sisal-kernel language. The second result is an extension of C-kernel axiomatic semantics by inference rule for Cloud-Sisal-kernel loops. The paper also presents our approach to the problem of deductive verification automation in the case of finite iterations over data structures. This kind of loops is referred to as definite iterations. Our solution is a composition of symbolic method of verification of definite iterations, verification condition metageneration and mixed axiomatic semantics method. Symbolic method of verification of definite iterations allows defining inference rules for these loops without invariants. Symbolic replacement of definite iterations by recursive functions is the base of this method. Obtained verification conditions with applications of recursive functions correspond to logical base of ACL2 prover. We use ACL2 system based on computable recursive functions. Verification condition metageneration allows simplifying implementation of new inference rules in a verification system. The use of mixed axiomatic semantics results to simpler verification conditions in some cases.

Explanatory Power for Medical Expert Systems: Studies in the Representation of Causal Relationships for Clinical Consultations

1982 ◽  
Vol 21 (03) ◽  
pp. 127-136 ◽  
Author(s):  
J. W. Wallis ◽  
E. H. Shortliffe
Keyword(s):  
Explanatory Power ◽  
Prototype System ◽  
Inference Rules ◽  
Medical Expert ◽  
Comprehensive Knowledge ◽  
Different Types ◽  
Medical Expert Systems ◽  
Explanation System ◽  
Systems Studies

This paper reports on experiments designed to identify and implement mechanisms for enhancing the explanation capabilities of reasoning programs for medical consultation. The goals of an explanation system are discussed, as is the additional knowledge needed to meet these goals in a medical domain. We have focussed on the generation of explanations that are appropriate for different types of system users. This task requires a knowledge of what is complex and what is important; it is further strengthened by a classification of the associations or causal mechanisms inherent in the inference rules. A causal representation can also be used to aid in refining a comprehensive knowledge base so that the reasoning and explanations are more adequate. We describe a prototype system which reasons from causal inference rules and generates explanations that are appropriate for the user.

On Statman's Finite Completeness Theorem

1992 ◽  
Author(s):  
Richard Statman ◽  
Gilles Dowek
Keyword(s):  
Completeness Theorem
Sign in / Sign up

Export Citation Format

Share Document