Interpretation of Probabilistic Algorithmic Logic in Nondeterministic Algorithmic Logic

2007 ◽  
Author(s):  
Agnieszka Makarec
Keyword(s):  
Algorithmic Logic

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.

Retrieval System and Dynamic Algorithm Looking for Axioms of Notions Defined by Programs

1993 ◽  
Vol 19 (3-4) ◽  
pp. 275-301
Author(s):  
Andrzej Biela
Keyword(s):  
Theorem Proving ◽  
Dynamic Process ◽  
Functional Equations ◽  
Automated Theorem Proving ◽  
Retrieval System ◽  
Formal System ◽  
Dynamic Algorithm ◽  
Algorithmic Logic ◽  
Correctness Of Programs

In this paper we shall introduce a formal system of algorithmic logic which enables us to formulate some problems connected with a retrieval system which provides a comprehensive tool in automated theorem proving of theorems consisting of programs, procedures and functions. The procedures and functions may occur in considered theorems while the program of the above mentioned system is being executed. We can get an answer whether some relations defined by programs hold and we can prove functional equations in a dynamic way by looking for a special set of axioms /assumptions/ during the execution of system. We formulate RS-algorithm which enables us to construct the set of axioms for proving some properties of functions and relations defined by programs. By RS-algorithm we get the dynamic process of proving functional equations and we can answer the question whether some relations defined by programs hold. It enables us to solve some problems concerning the correctness of programs. This system can be used for giving an expert appraisement. We shall provide the major structures and a sketch of an implementation of the above formal system.

Investigations of properties of programs by means of the extended algorithmic logic I

1977 ◽  
Vol 1 (1) ◽  
pp. 93-119
Author(s):  
Lech Banachowski
Keyword(s):  
Mathematical Model ◽  
Mathematical Tool ◽  
Methods Of Analysis ◽  
Semantic Correctness ◽  
Algorithmic Logic ◽  
Correctness Of Programs

The present paper contains investigations concerning the semantic correctness of programs. Presented methods of analysis of programs are appropriate for every domain of computation. Algorithmic logic extended by classical quantifiers is a fundamental mathematical tool used in the paper. Interrelations between properties of programs and properties of descriptions of programs are studied (a description of a program is a mathematical model of the notion of a documentation of a program).

Algorithmic Logic with Stacks and Its Model-Theoretical Properties

1984 ◽  
Vol 7 (4) ◽  
pp. 391-428
Author(s):  
Wiktor Dańko
Keyword(s):  
Second Order ◽  
Order Logic ◽  
Algorithmic Logic ◽  
Second Order Logic

In this paper we propose to transform the Algorithmic Theory of Stacks (cf. Salwicki [30]) into a logic for expressing and proving properties of programs with stacks. We compare this logic to the Weak Second Order Logic (cf. [11, 15]) and prove theorems concerning axiomatizability without quantifiers (an analogon of Łoś-Tarski theorem) and χ 0 - categoricity (an analogon of Ryll-Nardzewski’s theorem).

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.

APC: The Algorithmic Predicate Calculus

1981 ◽  
Vol 4 (2) ◽  
pp. 343-367
Author(s):  
Wojciech Przyłuski
Keyword(s):  
Time Scale ◽  
Predicate Calculus ◽  
Algorithmic Logic ◽  
Classical Predicate

The paper presents a logic which is an algorithmic extension of the classical predicate calculus and is based on the ideas given by F. Kröger. The programs and the effects of their execution are the formulas of this logic which are considered at any time scale. There are many interesting properties of the logic which are connected with the notion of time scale. These properties are examined in the paper. Moreover the problem of the formulas normalization is presented. Our logic is compared with the algorithmic logic introduced by A. Salwicki. Next, the usefulness of a new logic in the theory of programs is shown.

Sign in / Sign up

Export Citation Format

Share Document