Kleene Theorem in Partial Conway Theories with Applications

2011 ◽  
pp. 72-93
Author(s):  
Zoltán Ésik ◽  
Tamás Hajgató
Keyword(s):  
Kleene Theorem

scholarly journals A KLEENE THEOREM FOR LANGUAGES OF WORDS INDEXED BY LINEAR ORDERINGS

2006 ◽  
Vol 17 (03) ◽  
pp. 519-541 ◽  
Author(s):  
ALEXIS BÈS ◽  
OLIVIER CARTON
Keyword(s):  
Preceding Paper ◽  
Linear Orderings ◽  
Rational Expressions ◽  
Kleene Theorem

In a preceding paper, Bruyère and Carton introduced automata, as well as rational expressions, which allow to deal with words indexed by linear orderings. A Kleene-like theorem was proved for words indexed by countable scattered linear orderings. In this paper we extend this result to languages of words indexed by all linear orderings.

scholarly journals A Kleene theorem and model checking algorithms for existentially bounded communicating automata

2006 ◽  
Vol 204 (6) ◽  
pp. 920-956 ◽  
Author(s):  
Blaise Genest ◽  
Dietrich Kuske ◽  
Anca Muscholl
Keyword(s):  
Model Checking ◽  
Communicating Automata ◽  
Kleene Theorem

scholarly journals A Kleene theorem for weighted tree automata over tree valuation monoids

2019 ◽  
Vol 269 ◽  
pp. 104445 ◽  
Author(s):  
Doreen Götze ◽  
Zoltán Fülöp ◽  
Manfred Droste
Keyword(s):  
Tree Automata ◽  
Weighted Tree ◽  
Weighted Tree Automata ◽  
Kleene Theorem

scholarly journals Inductive * -Semirings

2000 ◽  
Vol 7 (27) ◽  
Author(s):  
Zoltán Ésik ◽  
Werner Kuich
Keyword(s):  
Fixed Point ◽  
Power Series ◽  
Computer Science ◽  
Equational Theory ◽  
Star Operation ◽  
Rational Power Series ◽  
Fixed Point Equation ◽  
Point Equation ◽  
Regular Sets ◽  
Kleene Theorem

One of the most well-known induction principles in computer science<br />is the fixed point induction rule, or least pre-fixed point rule. Inductive <br />*-semirings are partially ordered semirings equipped with a star operation<br />satisfying the fixed point equation and the fixed point induction rule for<br />linear terms. Inductive *-semirings are extensions of continuous semirings<br />and the Kleene algebras of Conway and Kozen.<br />We develop, in a systematic way, the rudiments of the theory of inductive<br />*-semirings in relation to automata, languages and power series.<br />In particular, we prove that if S is an inductive *-semiring, then so is<br />the semiring of matrices Sn*n, for any integer n >= 0, and that if S is<br />an inductive *-semiring, then so is any semiring of power series S((A*)).<br />As shown by Kozen, the dual of an inductive *-semiring may not be inductive. <br />In contrast, we show that the dual of an iteration semiring is<br />an iteration semiring. Kuich proved a general Kleene theorem for continuous<br /> semirings, and Bloom and Esik proved a Kleene theorem for all Conway <br />semirings. Since any inductive *-semiring is a Conway semiring<br />and an iteration semiring, as we show, there results a Kleene theorem <br />applicable to all inductive *-semirings. We also describe the structure<br />of the initial inductive *-semiring and conjecture that any free inductive<br />*-semiring may be given as a semiring of rational power series with <br />coefficients in the initial inductive *-semiring. We relate this conjecture to<br />recent axiomatization results on the equational theory of the regular sets.

scholarly journals A Machine-Level Interpretation of Deductive Rules on Enact I and Enact II Model Theorems.

2020 ◽  
Keyword(s):  
Theorem Proving ◽  
Research Proposal ◽  
Reading And Writing ◽  
Axiom Schema ◽  
Deduction Rules ◽  
Kleene Theorem

This research proposal is on provable forms based on s yntactic theorem using Kleene Axiom schema. Enact model I and II of propositional formulas from enactment logic are proven in terms of theorems based on deductive rules. Work proves by deduction rules that Enact Model I and II are model theorems[1] in machinelevel interpretation. Enactprover is a machine program for reading and writing Kleene theorem proving axioms based one enactment logic.

Sign in / Sign up

Export Citation Format

Share Document