Wyniki wyszukiwania - BazTech

1

On Axiomatizability of the Multiplicative Theory of Numbers

Salehi S.

Fundamenta Informaticae

|

2018

|

Vol. 159, nr 3

279--296

EN

The multiplicative theory of a set of numbers (which could be natural, integer, rational, real or complex numbers) is the first-order theory of the structure of that set with (solely) the multiplication operation (that set is taken to be multiplicative, i.e., closed under multiplication). In this paper we study the multiplicative theories of the complex, real and (positive) rational numbers. These theories (and also the multiplicative theories of natural and integer numbers) are known to be decidable (i.e., there exists an algorithm that decides whether a given sentence is derivable form the theory); here we present explicit axiomatizations for them and show that they are not finitely axiomatizable. For each of these sets (of complex, real and [positive] rational numbers) a language, including the multiplication operation, is introduced in a way that it allows quantifier elimination (for the theory of that set).

2

Proving Theorems by Program Transformation

Fioravanti F., Pettorossi A., Proietti M., Senni V.

Fundamenta Informaticae

|

2013

|

Vol. 127, nr 1-4

115--134

EN

In this paper we present an overview of the unfold/fold proof method, a method for proving theorems about programs, based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming (CLP), and we present a set of transformation rules (including the familiar unfolding and folding rules) which preserve the semantics of CLP programs. Then, we show how program transformation strategies can be used, similarly to theorem proving tactics, for guiding the application of the transformation rules and inferring the properties to be proved. We work out three examples: (i) the proof of predicate equivalences, applied to the verification of equality between CCS processes, (ii) the proof of first order formulas via an extension of the quantifier elimination method, and (iii) the proof of temporal properties of infinite state concurrent systems, by using a transformation strategy that performs program specialization.

3

Automated Generation of Logical Constraints on Approximation Spaces Using Quantifier Elimination

Doherty P., Szałas A.

Fundamenta Informaticae

|

2013

|

Vol. 127, nr 1-4

135--149

EN

This paper focuses on approximate reasoning based on the use of approximation spaces. Approximation spaces and the approximated relations induced by them are a generalization of the rough set-based approximations of Pawlak. Approximation spaces are used to define neighborhoods around individuals and rough inclusion functions. These in turn are used to define approximate sets and relations. In any of the approaches, one would like to embed such relations in an appropriate logical theory which can be used as a reasoning engine for specific applications with specific constraints. We propose a framework which permits a formal study of the relationship between properties of approximations and properties of approximation spaces. Using ideas from correspondence theory, we develop an analogous framework for approximation spaces. We also show that this framework can be strongly supported by automated techniques for quantifier elimination.

4

A model-theoretic version of the complement theorem : applications

Nowak K.

Bulletin of the Polish Academy of Sciences. Mathematics

|

1999

|

Vol. 47, no 4

355-361

EN

The paper treats of some consequences of the model-theoretic version of Gabrielov's complement theorem from [11], which asserts that the theories T[sub an] (introduced in [11] and T'[sub an] (defined herein) are model-complete. The theory T'[sub an] is a universal modification of T[sub an] in the language L'[sub an] of ordered rings expanded by the symbols of restricted analytic functions, arithmetic roots and multiplicative inverse l/x. We give a short proof of the curve selecting lemma, and next we demonstrate how quantifier elimination, within the structure R[sub an] expanded by multiplicative inverse 1/x (a result due to Denef-van den Dries [4], can be obtained from the complement theorem through a general method of logic. Also presented is an application to definability problems ; namely, a piecewise description of a subanalytic function by restricted analytic functions, arithmetic roots and l/x.

5

A model-theoretic criterion for quantifier elimination and its application to geometry

Nowak K.

Bulletin of the Polish Academy of Sciences. Mathematics

|

1998

|

Vol. 46, no 4

377-381

EN

In this paper we present a model-theoretic criterion for quantifier elimination being a variant of Shoenfield's theorem (see [1], Chap. V, [paragraph]5). Our short proof is based directly on Godel's completeness and compactness theorems as well as on the concept of diagrams, and does not involve model-completeness or Robinson's test as does for instance the proof of certain related criteria given in [2], Chap. VIII, [paragraph]4. As a consequence, we immediately obtain the theorems of Chevalley and Tarski-Seidenberg from algebraic and semialalgebraic geometry.