Solid codes and disjunctive domains.
Some Algebraic Properties of Machine Poset of Infinite Words
The complexity of infinite words is considered from the point of view of a transformation with a Mealy machine that is the simplest model of a finite automaton transducer. We are mostly interested in algebraic properties of the underlying partially ordered set. Results considered with the existence of supremum, infimum, antichains, chains and density aspects are investigated.
Some algorithms on the star operation applied to finite languages.
Some arithmetical theorems on base conversions
Some Characteristics of the Process Measure of the Amount of Information
Some closure properties of the nondeterministic regular translations.
Some combinatorial properties of complete semi-Thue systems.
Some consequences of a result of Ehrenfeucht and Rozenberg
Some fundamental notions of large variable systems
Some further remarks on the family of finite index matrix languages
Some further remarks on the index of context-free languages
Some geometric perspectives in concurrency theory.
Some graphic uses of an even number of odd nodes
Vertex-degree parity in large implicit “exchange graphs” implies some EP theorems asserting the existence of a second object without evidently providing a polytime algorithm for finding a second object.
Some hardness results for question/answer games.
Some issues in using formal methods for the development of reactive systems.
Some key research problems in automated theorem proving for hardware and software verification.
This paper sketches the state of the art in the application of mechanical theorem provers to the verification of commercial computer hardware and software. While the paper focuses on the theorem proving system ACL2, developed by the two authors, it references much related work in formal methods. The paper is intended to satisfy the curiosity of readers interested in logic and artificial intelligence as to the role of mechanized theorem proving in hardware and software design today. In addition,...
Some modifications of auxiliary pushdown automata
Some problems in automata theory which depend on the models of set theory
We prove that some fairly basic questions on automata reading infinite words depend on the models of the axiomatic system ZFC. It is known that there are only three possibilities for the cardinality of the complement of an ω-language L(x1d49c;) accepted by a Büchi 1-counter automaton x1d49c;. We prove the following surprising result: there exists a 1-counter Büchi automaton x1d49c; such that the cardinality of the complement L(𝒜) − of the ω-language L(𝒜) is not determined...
Some problems in automata theory which depend on the models of set theory
We prove that some fairly basic questions on automata reading infinite words depend on the models of the axiomatic system ZFC. It is known that there are only three possibilities for the cardinality of the complement of an ω-language L(𝒜) accepted by a Büchi 1-counter automaton 𝒜. We prove the following surprising result: there exists a 1-counter Büchi automaton 𝒜 such that the cardinality of the complement L(𝒜) − of the ω-language L(𝒜) is not determined by ZFC: (1) There is a model V1...
Some problems in modelling of real systems by formalized ones