TY - JOUR

T1 - A Language Using Quantifiers for Description of Assertions about Some Number Total Functions

AU - Kosovskii, N.

PY - 2014

Y1 - 2014

N2 - Mathematical models of N-finite (N  2) (especially for N= 216 typical for IBM-compatible personal computers) real, integer or boolean valued computations are proposed in the frameworks of a finite-discrete mathematics. Such a mathematical model more precisely characterizes the contemporary practice of the computer use. Notions of an N-finite RAM (Random Access Machine), an N-finite RASP (Random Access Machine with Stored Program) and an N-finite Pascal program using integer operations modulo N with the reminders from the segment [–N/2, N/2 – 1 + (N mod 2)] are introduced. A formal N-finite quantifier logic language of modulo N arithmetic operations is defined. It allows to formulate mathematical properties of such a non-recursive total Pascal function or predicate. It is proved that the problem of a formula identical truth in such a language containing arithmetic operations modulo N is a P-SPACE-complete one. So, the proof of a correctness of a non-recursive total Pascal program may be simplified with t

AB - Mathematical models of N-finite (N  2) (especially for N= 216 typical for IBM-compatible personal computers) real, integer or boolean valued computations are proposed in the frameworks of a finite-discrete mathematics. Such a mathematical model more precisely characterizes the contemporary practice of the computer use. Notions of an N-finite RAM (Random Access Machine), an N-finite RASP (Random Access Machine with Stored Program) and an N-finite Pascal program using integer operations modulo N with the reminders from the segment [–N/2, N/2 – 1 + (N mod 2)] are introduced. A formal N-finite quantifier logic language of modulo N arithmetic operations is defined. It allows to formulate mathematical properties of such a non-recursive total Pascal function or predicate. It is proved that the problem of a formula identical truth in such a language containing arithmetic operations modulo N is a P-SPACE-complete one. So, the proof of a correctness of a non-recursive total Pascal program may be simplified with t

KW - P-SPACE-completeness

KW - RAM

KW - RASP

KW - Pascal

KW - correctness of a Pascal program

M3 - Article

VL - 21

SP - 120

EP - 125

JO - International Journal on Information Theory and Applications

JF - International Journal on Information Theory and Applications

SN - 1310-0513

IS - 2

ER -