Search Results

1 - 9 of 9 items :

• "partial predicate"
Clear All
OPEN ACCESS

Summary

We show that the set of all partial predicates over a set D together with the disjunction, conjunction, and negation operations, defined in accordance with the truth tables of S.C. Kleene’s strong logic of indeterminacy [], forms a Kleene algebra. A Kleene algebra is a De Morgan algebra [] (also called quasi-Boolean algebra) which satisfies the condition x¬:xy¬ :y (sometimes called the normality axiom). We use the formalization of De Morgan algebras from [].

The term “Kleene algebra” was introduced by A. Monteiro and D. Brignole in []. A similar notion of a “normal i-lattice” had been previously studied by J.A. Kalman []. More details about the origin of this notion and its relation to other notions can be found in [, , , ]. It should be noted that there is a different widely known class of algebras, also called Kleene algebras [, ], which generalize the algebra of regular expressions, however, the term “Kleene algebra” used in this paper does not refer to them.

Algebras of partial predicates naturally arise in computability theory in the study on partial recursive predicates. They were studied in connection with non-classical logics [, , , , , ]. A partial predicate also corresponds to the notion of a partial set [] on a given domain, which represents a (partial) property which for any given element of this domain may hold, not hold, or neither hold nor not hold. The field of all partial sets on a given domain is an algebra with generalized operations of union, intersection, complement, and three constants (0, 1, n which is the fixed point of complement) which can be generalized to an equational class of algebras called DMF-algebras (De Morgan algebras with a single fixed point of involution) []. In [] partial sets and DMF-algebras were considered as a basis for unification of set-theoretic and linguistic approaches to probability.

Partial predicates over classes of mathematical models of data were used for formalizing semantics of computer programs in the composition-nominative approach to program formalization [, , , ], for formalizing extensions of the Floyd-Hoare logic [, ] which allow reasoning about properties of programs in the case of partial pre- and postconditions [, , , ], for formalizing dynamical models with partial behaviors in the context of the mathematical systems theory [, , , , ].

, Nick Bassiliades, Hans-Georg Fill, Vitaliy Yakovyna, Heinrich C. Mayr, Vyacheslav Kharchenko, Vladimir Peschanenko, Mariya Shyshkina, Mykola Nikitchenko, and Aleksander Spivakovsky, editors, Proceedings of the 13th International Conference on ICT in Education, Research and Industrial Applications. Integration, Harmonization and Knowledge Transfer, Kyiv, Ukraine, May 15–18, 2017 , volume 1844 of CEUR Workshop Proceedings , pages 504–523. CEUR-WS.org, 2017. [8] Artur Korniłowicz, Ievgen Ivanov, and Mykola Nikitchenko. Kleene algebra of partial predicates. Formalized

Information Systems, FedCSIS 2017, Prague, Czech Republic, September 3–6, 2017. , pages 237–244, 2017. ISBN 978-83-946253-7-5. doi:10.15439/2017F301. [12] Artur Korniłowicz, Ievgen Ivanov, and Mykola Nikitchenko. Kleene algebra of partial predicates. Formalized Mathematics , 26( 1 ):11–20, 2018. doi:10.2478/forma-2018-0002. [13] Artur Korniłowicz, Andrii Kryvolap, Mykola Nikitchenko, and Ievgen Ivanov. Formalization of the nominative algorithmic algebra in Mizar. In Jerzy Świątek, Leszek Borzemski, and Zofia Wilimowska, editors, Information Systems Architecture and

Proceedings , pages 504–523. CEUR-WS.org, 2017. [12] Andrii Kryvolap, Mykola Nikitchenko, and Wolfgang Schreiner. Extending Floyd-Hoare Logic for Partial Pre- and Postconditions , pages 355–378. Springer International Publishing, 2013. ISBN 978-3-319-03998-5. doi:10.1007/978-3-319-03998-5_18. [13] Mykola Nikitchenko and Andrii Kryvolap. Properties of inference systems for Floyd-Hoare logic with partial predicates. Acta Electrotechnica et Informatica , 13(4):70–78, 2013. doi:10.15546/aeei-2013-0052. [14] Mykola S. Nikitchenko. Composition-nominative aspects of address

OPEN ACCESS

, Artur Korniłowicz, and Mykola Nikitchenko. Implementation of the composition-nominative approach to program formalization in Mizar. The Computer Science Journal of Moldova , 26(1):59–76, 2018. [6] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. On an algorithmic algebra over simple-named complex-valued nominative data. Formalized Mathematics , 26(2):149–158, 2018. doi:10.2478/forma-2018-0012. [7] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. An inference system of an extension of Floyd-Hoare logic for partial predicates. Formalized Mathematics

OPEN ACCESS

, 26( 2 ):149–158, 2018. doi:10.2478/forma-2018-0012. [9] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. An inference system of an extension of Floyd-Hoare logic for partial predicates. Formalized Mathematics , 26( 2 ): 159–164, 2018. doi:10.2478/forma-2018-0013. [10] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. Partial correctness of GCD algorithm. Formalized Mathematics , 26( 2 ):165–173, 2018. doi:10.2478/forma-2018-0014. [11] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. On algebras of algorithms and specifications over

OPEN ACCESS

, 26( 2 ):149–158, 2018. doi:10.2478/forma-2018-0012. [9] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. An inference system of an extension of Floyd-Hoare logic for partial predicates. Formalized Mathematics , 26( 2 ): 159–164, 2018. doi:10.2478/forma-2018-0013. [10] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. On algebras of algorithms and specifications over uninterpreted data. Formalized Mathematics , 26( 2 ):141–147, 2018. doi:10.2478/forma-2018-0011. [11] Artur Kornilowicz, Andrii Kryvolap, Mykola Nikitchenko, and Ievgen Ivanov

OPEN ACCESS

, 26( 2 ):149–158, 2018. doi:10.2478/forma-2018-0012. [9] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. An inference system of an extension of Floyd-Hoare logic for partial predicates. Formalized Mathematics , 26( 2 ): 159–164, 2018. doi:10.2478/forma-2018-0013. [10] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. Partial correctness of GCD algorithm. Formalized Mathematics , 26( 2 ):165–173, 2018. doi:10.2478/forma-2018-0014. [11] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. On algebras of algorithms and specifications over

algebra of partial predicates. Formalized Mathematics , 26( 1 ):11–20, 2018. doi:10.2478/forma-2018-0002. [12] Artur Korniłowicz, Andrii Kryvolap, Mykola Nikitchenko, and Ievgen Ivanov. Formalization of the nominative algorithmic algebra in Mizar. In Jerzy Świątek, Leszek Borzemski, and Zofia Wilimowska, editors, Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology – ISAT 2017: Part II , pages 176–186. Springer International Publishing, 2018. ISBN 978-3-319-67229-8. doi:10