bluuebunny/crossref_metadata_2025 huggingface dataset:
RANK 2 INTERSECTION TYPE ASSIGNMENT IN TERM REWRITING SYSTEMS
Authors: Bakel Steffen van
Published: December 2019

A notion of type assignment on Curryfied Term Rewriting Systems is introduced that uses Intersection Types of Rank 2, and in which all function symbols are assumed to have a type. Type assignment will consist of specifying derivation rules that describe how types can be assigned to terms, using the types of function symbols. Using a modified unification procedure, for each term the principal pair (of basis and type) will be defined in the following sense: from these all admissible pairs can be generated by chains of operations on pairs, consisting of the operations substitution, copying, and weakening. In general, given an arbitrary typeable GTRS, the subject reduction property does not hold. Using the principal type for the left-hand side of a rewrite rule, a sufficient and decidable condition will be formulated that typeable rewrite rules should satisfy in order to obtain this property.
McCARTHY ALGEBRAS: A MODEL OF McCARTHY'S LOGICAL CALCULUS
Authors: Konikowska Beata
Published: December 2019

The paper introduces a notion of an algebra corresponding to the three-valued logical calculus designed by McCarthy for computation purposes and used in several existing software system. The algebra, called McCarthy algebra, is a generalization of a Boolean algebra. It is defined extensionally, but a set of sound equality axioms is also given. From these axioms, various non-classical properties of the elements of such algebras are deduced. A representation theorem for two classes of McCarthy algebras is presented.
EXPANDING GRAPH RELABELING SYSTEMS HAVE THE POWER OF RECURSIVE ENUMERABILITY
Authors: Sopena Eric
Published: December 2019

Graph relabeling systems (GRS's) have been introduced as a suitable tool for coding and proving sequential or distributed algorithms on graphs or networks. These systems do not change the underlying structure of the graph on which they work, but only the labeling of its components (edges or vertices). Each relabeling step is fully determined by the knowledge of a fixed size subgraph, the relabeled occurrence. We introduce an extension of that model, the so-called expanding graph relabeling systems (e-GRS's), which allows the generation of sets of graphs by means of component relabeling. We study the generating power of these systems and prove that they enable us to generate any recursively enumerable set of graphs. We first show how the “from left to right” natural orientation of a string-graph, that is a graph representation of a string, can be translated by means of vertex labels in such a way that any local transformation of the string can be simulated by a local relabeling of the string-graph vertices. Using this translation, we show that any phrase-structure string grammar can be simulated by an e-GRS. Finally, we provide a way of encoding graphs as strings and an e-GRS, called the decoder, which can convert any string representation of the encoding of a graph into the graph itself.
PARALLEL WORD SUBSTITUTION
Authors: La Torre Salvatore , Napoli Margherita , Parente Domenico
Published: December 2019

We study the parallel word substitution operation: in a text t, all non overlapping occurrences of a word ω are simultaneously substituted in each possible decomposition of t with respect to ω. We give necessary conditions on the reversibility of t under parallel word substitution.
CATEGORISATION OF COMPUTABLE DATABASE QUERIES
Authors: Levene Mark , Loizou George
Published: December 2019

We present an alternative approach to that of Chandra and Harel [5] and Abiteboul and Vianu [1] in considering computable database queries, which are mappings from sets of records to sets of records. In particular, we view a computable database query as being realised via a Turing-computable mapping from strings to strings and an encoding, which encodes the input set of records into an appropriate string. An encoding of a set of records consists of two components: an ordering function, which orders the records in a set as well as the values of each record in the set, and an isomorphism, which maps the values in the records of the set to strings. An important class of encodings, called free encodings, whose isomorphism has the same semantics as the identity mapping on record values, is also defined. Our analysis of computable database queries elucidates the notion of a computable database query by dealing with the problem of how a database language can be implemented on a standard Turing machine that does not cater directly for mappings from sets of records to sets of records. We carry out our analysis by categorising computable database queries into subclasses and by establishing the relationships that exist amongst these subclasses. We also investigate an equivalence relation on computable database queries; two computable database queries are related if they are realised via the same Turing-computable mapping, say δ. We prove the following interesting result regarding the cardinality of the equivalence class of a computable query with respect to the said equivalence relation: either δ does not realise any computable query, or δ realises exactly one computable query, or δ realises a countably infinite set of computable queries. Our final result shows that, by adding membership queries to the class of encoding-independent computable queries, the closure of the resulting extended class under composition of mappings is the set of all isomorphism-independent computable queries.
ABDUCTIVE CHANGE OPERATORS
Authors: Lobo Jorge , Uzcátegui Carlos
Published: December 2019

This paper describes a change theory based on abductive reasoning. We take the AGM postulates for revisions, expansions and contractions, and Katsuno and Mendelzon postulates for updates and incorporate abduction into them. A key feature of the theory is that presents a unified view of standard change operators and abductive change operators rather than a new and independent change theory for abductive changes. Abductive operators reduce to standard change operators in the limiting cases.
(0,1)-TOTALITY IS UNDECIDABLE FOR ARBITRARY CONTEXT-FREE GRAMMARS
Authors: Mäkinen Erkki
Published: December 2019

This note shows that it is undecidable whether or not an arbitrary context-free grammar is (0,l)-total, i.e., whether or not {0, 1}+ ⊆ g(Szl(G)) holds for an arbitrary context-free grammar G, the left Szilard language Szl(G) of G, and a homomorphism g mapping the labels of G's productions into {0, 1} ∪ {λ}. These considerations are motivated by cryptosystems recently proposed by Andrasiu et al.
ON USING SEMI-DYCK SETS TO ANALYSE COUPLED-CONTEXT-FREE LANGUAGES
Authors: Hotz Günter , Pitsch Gisela
Published: December 2019

Coupled-Context-Free Grammars are a natural generalization of context-free grammars obtained by combining nonterminals to corresponding parentheses which can only be substituted simultaneously. Refering to their generative capacity we obtain an infinite hierarchy of languages that comprises the context-free ones as the first and all those generated by Tree Adjoining Grammars (TAGs) as the second element. The latter is important because today, TAGs are commonly used to model the syntax of natural languages. Here, we present a completely new approach to analyse this language hierarchy. It solves the word problem for the class of languages generated by TAGs in time O(n6), n length of the input, by reducing it to the analysis of sequences of parentheses.
MECHANIZATION OF REAL-TIME LINEAR CSP WITH HIGHER ORDER LOGIC
Authors: Peters James F.
Published: December 2019

A linear form of Reed-Roscoe Timed Communicating Sequential Processes mechanized with the Higher Order Logic Proof System is presented. The syntax for the Real-Time Linear CSP (RTLCSP) language is sufficient to describe the behavior of time-constrained communicating processes in real-time systems. The operational semantics of RTLCSP is expressed in terms of inference rules and Coloured Hierarchical Petri nets for a transition system for real-time programs. RTLCSP processes are characterized in terms of an extension of the Lynch-Tuttle signature for communicating processes. The signature of a process is helpful in reasoning about process behavior and in defining the semantics of empty processes or processes with hidden actions. The linear character of RTLCSP stems from its resource consciousness inasmuch as restrictions are placed on the number of times that a process can be restarted. The complete mechanization of RTLCSP in HOL (called RTLCSP-HOL) is presented in detail. The presentation includes a brief introduction to HOL itself to permit experimentation with RTLCSP-HOL. Sample HOL proofs relative to RTLCSP constructs are also given.
ON DEFINITIONAL TRANSFORMATIONS TO NORMAL FORM FOR INTUITIONISTIC LOGIC
Authors: Egly Uwe
Published: December 2019

In this paper, we examine different definitional transformations into normal form for intuitionistic logic. In contrast to the classical case, “intuitionistic clauses” may contain implications and quantifiers. Usually, such definitional transformations introduce labels defining subfor-mulae. An obvious optimization is the use of implications instead of equivalences whenever possible, which can reduce the size of the resulting normal form. We compare the optimized transformation with the unoptimized transformation with respect to the shortest cut-free LJ-derivation of the resulting normal forms. The comparison is based on a sequence (Hk)k∈N of formulae for which the following hold: (i) there exist cut-free LJ-proofs of the unoptimized normal form of Hk with length double-exponential in k, and (ii) any cut-free LJ-proof of the optimized normal form of Hk has length non-elementary in k. The reason for the different behaviour is the simulation of analytic cuts by the unoptimized translation, which is not possible when the optimization is applied.
CHOMSKY HIERARCHY AND SYSTOLIC Y-TREE AUTOMATA
Authors: Fachini Emanuela , Monti Angelo
Published: December 2019

We prove that no nonregular deterministic context-free language is accepted by any systolic Y-tree automaton while some of them, but not all, can be accepted by nondeterministic systolic Y-tree automata. We show that weak superstable systolic automata over incomplete Y-tree can accept only regular languages. We also show that the weak superstability and the superstability problems are decidable for deterministic systolic automata over a sparse and superprefix Y-tree. Moreover we prove that the regularity problem is decidable for systolic binary tree automata.
A NEW METHOD OF CIRCUMSCRIBING BELIEFS THE PROPOSITIONAL CASE
Authors: Kundu Sukhamay , Chen Jianhua
Published: December 2019

We propose here a new notion of a minimal model for forming circumscription in belief-logic by incorporating the notion of minimal models in the prepositional logic. This results in a new circumscription operation for belief-formulas than the one considered in [4-6]. An important feature of the new circumscription operation is its close relationship with the circumscription of prepositional formulas. For instance, we have CIRC[Bφ] = B(CIRC[φ]), where φ is a prepositional formula. We give several examples to show that the new notion of circumscription fits quite well with intuition.
On the Decidability of Non-Interleaving Process Equivalences
Authors: Kiehn Astrid , Hennessy Matthew
Published: December 2019

We develop decision procedures based on proof tableaux for a number of non-interleaving equivalences over processes. The processes considered are those which can be described in a simple extension of BPPr, Basic Parallel Processes with communication, obtained by omitting the restriction operator from CCS. Decision procedures are given for both strong and weak versions of location equivalence and ST-bisimulation.
Some Undecidability Results For Finitely Generated Thue Congruences On A Two-Letter Alphabet
Authors: Madlener Klaus , Otto Friedrich
Published: December 2019

Following the course set by A. Markov (1951), S. Adjan (1958), and M. Rabin (1958), C. Ó'Dúnlaing (1983) has shown that certain properties of finitely generated Thue congruences are undecidable in general. Here we prove that many of these undecidability results remain valid even when only finitely generated Thue congruences on a fixed two-letter alphabet Σ2 are considered. In contrast to a construction given by P. Schupp (1976) which applies to groups only, we use a modified version of a technical lemma from A. Markov's original paper. Based on this technical result we can carry the result of A. Sattler-Klein (1996), which says that certain Markov properties remain undecidable even when they are restricted to finitely generated Thue congruences that are decidable, over to the alphabet Σ2.
Deriving Invariants and Constraints from Action Theories
Authors: Zhang Yan , Foo Norman Y.
Published: December 2019

Recent work on reasoning about action has shown that there exists an interesting connection between action specifications and state constraints — it is possible to extract state constraints from action specifications. This work provides us another way to describe the behaviour of dynamic systems. In this paper, we address the problem of generating action invariants from action specifications, and generalizing action invariants into state constraints. We first propose a persistence-based formalism of actions, and show that the generation of action invariants is achieved from action specifications by reasoning about persistence. We then investigate the generalization of action invariants into state constraints. Blocks world examples illustrate the general procedure throughout.
Some Techniques of Reducing the Dangers of Combinatorial Explosion in Automatic Knowledge Acquisition
Authors: Findler Nicholas V.
Published: December 2019

The danger of getting into a combinatorial explosion has remained probably the most serious impediment to using knowledge-based systems for real-life problems. Justifiable heuristics must cut down the size of potentially huge search spaces to a realistic and manageable size - without jeopardizing the success of finding satisfactory solutions. This paper describes some techniques that have proved to be effective in the operation of two different systems: the Quasi-Optimizer (QO) and the Generalized Production Rule System (GPRS). The QO is a domain-independent automatic knowledge acquisition tool that can obtain, verify, fuse and optimize human expertise. It generates computer models, descriptive theories, of human decision making strategies, and can also select and combine the best components of several such models into a single strategy which may be considered a normative theory in the statistical sense. The techniques developed to reduce the danger of combinatorial explosion with the QO include selecting the most independent (near-orthogonal) decision variables, chunking conceptually coherent decision variables, eliminating statistical outlier values, and using dynamically evolving experimental designs to result in a near-uniform reliability distribution of the strategy responses. The GPRS can estimate/predict values of hidden variables and can thus serve as a module of an expert system in need of numerical or functional estimates of hidden variable values. (Hidden variables can be observed and measured only intermittently and at irregular points of time and space – in contrast with open variables whose values can be identified at any time and location.) The estimation is based on generalized production rules expressing stochastic and potentially causal relations between known values of hidden variables and certain mathematical properties of the open variable distribution. A multi-dimensional learning process adds to, consolidates and optimizes the generalized rule base. It gradually merges “similar enough” production rules, and eliminates spurious and statistically not justifiable ones. Such processes reduce the danger of combinatorial explosions in knowledge acquisition. Finally, we note that human decision makers appear to resort to similar methods, although in a less systematic manner, when they are confronted with very large decision spaces.
On The Computational Complexity of Marcus Contextual Languages
Authors: Ilie Lucian
Published: December 2019

We investigate the computational complexity of the basic type of contextual languages, that is, the ones introduced by Marcus and called subsequently external contextual languages. We prove that the family of languages generated by external contextual grammars with context-free selection contains only polynomial time parsable languages.
Pattern Ambiguities for Pure Context—Free Grammars
Authors: Mäkinen Erkki , Ţiplea Ferucio Laurenţiu
Published: December 2019

We consider here some special forms of ambiguity for pure context-free grammars, namely pattern avoiding ambiguity, pattern preserving ambiguity, pattern ambiguity, and grammar avoiding ambiguity. The first two properties are undecidable for arbitrary pure context-free grammars, and in a particular but general enough case we can effectively decide whether or not a pure context-free grammar is pattern preserving ambiguous.
On a Hierarchy of Slender Languages Based on Control Sets
Authors: Koshiba Takeshi
Published: December 2019

We study slender context-sensitive languages, i.e., those containing at most a constant number of words of each length. Recently, it was proved that every slender regular language can be described by a finite union of terms of the form uviw [9] and every slender context-free language can be described by a finite union of terms of the form uviwxiy [4, 10]. We show a hierarchy of slender languages which is properly contained in the family of context-sensitive languages and which starts with the family of slender context-free languages, or slender regular languages. Each slender context-sensitive language in the hierarchy can be described by a finite union of terms of the form x1yi 1x2yi 2 ··· xnyi nxn+1.
On Learning Decision Structures
Authors: Michalski Ryszard S. , Imam Ibrahim F.
Published: December 2019

A decision structure is a simple and powerful tool for organizing a decision process. It differs from a conventional decision tree in that its nodes are assigned tests that can be functions of the attributes, rather than single attributes; the branches stemming from a node can be assigned a subset of attribute values rather than a single attribute value (test outcome); and the leaves can be assigned one or more alternative decisions. We describe a methodology for learning decision structures from declarative knowledge expressed in the form of decision rules. The decision rules are generated by an expert, or by an AQ-type inductive learning program (with or without constructive induction). From a given set of rules, one can generate many different decision structures. The proposed methodology generates the one that is most suitable for the given decision-making situation, according to a multicriterion evaluation function. Experiments with a program implementing the proposed methodology have demonstrated its many useful features.
Extension Rule for Non-Clausal Propositional Calculus
Authors: Majorinc Kazimir
Published: December 2019

Van Gelder has described a few reasons for satisfiability testing without transformation of formulas into CNF and has developed an algorithm for this problem. We have introduced two possible improvements. First, we have used directed acyclic graphs for the representation of formula, instead of representation in the form of a tree or a string of characters. Second, we have allowed a limited introduction of new variables, again without transformation to CNF. In terms of a proof system, Van Gelder’s algorithm does not p-simulate system described here. Some generalizations of notions of propositional formula, satisfiability, etc. are introduced.
An Abstract Approach to Some Loop Detection Problems
Authors: Skordev Dimiter
Published: December 2019

The abstract approach proposed here encompasses both the detection of some periodic loops during the execution of Prolog programs and the detection of some periodic loops during recursive computations (an attempt to look at the loop detection problem for Prolog from an abstract point of view has been done previously in a paper by the same author published in 1993).
Well-Founded Semantics for Default Logic
Authors: Brewka Gerhard , Gottlob Georg
Published: December 2019

Default logic is one of the most popular approaches to model defeasible reasoning. Nevertheless, there are a number of problems with Reiter's original semantics that have led to the investigation of alternative approaches. In particular, Baral/Subrahmanian and Przymusinska/Przymusinski have investigated generalizations of well-founded semantics for normal logic programs to default logic. These generalizations have a number of interesting properties. Unfortunately, it turns out that in many realistic situations they are unable to draw any defeasible conclusions at all - which can hardly be viewed as satisfactory. We show how this difficulty can be solved by varying the fixed point operator underlying the semantics. We define a range of different semantics. All of them are correct wrt. safe conclusions under Reiter semantics, i.e. those conclusions with the same proof in all extensions. For the strongest semantics we have also completeness in the case of coherent default theories, i.e. default theories with at least one extension. The logics differ in the effort spent for determining potential conclusions. It turns out that they are at least as complex as original default logic. We show that our approach also leads to new semantics for normal and extended logic programs. Moreover, we define prioritized versions of the logics.
Defining BDI with Abstract Languages
Authors: Burkhard Hans-Dieter
Published: December 2019

Mental attributes of agents are investigated in a framework of transition systems and abstract languages. The mental attitudes are related to beliefs, desires/goals and intentions/plans which are known from so-called BDI-architectures. Actions and events are more stressed than states. This allows the consideration of global and individual aspects of belief, desire, intentions etc. in a simple unified formalism.
The Block Product of Categories and Tilson's Division
Authors: Rey Jean-François
Published: December 2019

This paper introduces the notion of block product of two categories. It is the first step in the working out of a useful definition of the block product of two C-varieties which is needed for the theory of decompositions of monoids by means of wreath or block products. The construction of the block product of two categories is a particular case of a more general notion: the strong semidirect product of an action. In this first part of a two parts work we define the strong semidirect product functor and give some properties of this functor with respect to Tilson's division. In the second part we construct a left adjoint of the strong semidirect product functor and we define the kernel of a relational morphism of categories. With these notions we define the block product of two C-varieties and prove a kernel theorem in the category settings which extends a work of J. Rhodes and B. Tilson.
Fork Algebras in Algebra, Logic and Computer Science
Authors: Frias Marcelo F. , Baum Gabriel A. , Haeberer Armando M.
Published: December 2019

Since the main themes at the Helena Rasiowa memorial were algebra, logic and computer science, we will present a survey of results on fork algebras from these points of view. In this paper we study fork algebras from the points of view of their algebraic and logical properties and applications. These results will prove to be essential, in a future work, for the definition of a wide-spectrum calculus for program construction.
Queries and Algorithms Computable by Polynomial Time Existential Reflective Machines
Authors: Tyszkiewicz Jerzy
Published: December 2019

We consider two kinds of reflective relational machines: the usual ones, which use first order queries, and existential reflective machines, which use only first order existential queries. We compare these two computation models. We build on already existing results for standard relational machines, obtained by Abiteboul, Pa-padimitriou and Vianu [2], so we prove only results for existential machines. First we show that for both standard and existential reflective machines the set of polynomial time computable Boolean queries consists precisely of all 𝒫𝒮𝒫𝒜𝒞ℰ computable queries. Then we go further and compare which classes of algorithms both kinds of machines represent. Unless 𝒫𝒮𝒫𝒜𝒞ℰ = 𝒫𝒩𝒫, there are 𝒫𝒮𝒫𝒜𝒞ℰ queries which cannot be computed by polynomial time existential reflective machines which use only polynomial amount of relational memory, while it is possible for standard reflective machines. We conclude that existential reflective machines, being equivalent in computational power to unrestricted machines, implement substantially worse algorithms than the latter. Concerning deciding 𝒫 classes of structures, every fixpoint query can be evaluated by a polynomial time unrestricted reflective machine using constant number of variables, while existential reflective machines need [n/2] variables to implement the graph connectivity query. So again the algorithms represented by existential reflective machines are worse. Finally, for each k we get a characterization of the Δk+1p level in the polynomial time hierarchy in terms of reflective relational machines which use either Πk0 or Σkp queries.
A Convex Powerdomain over Lattices: its Logic and λ-Calculus
Authors: Alessi Fabio , Dezani-Ciancaglini Mariangiola , Liguoro Ugo de'
Published: December 2019

To model at the same time parallel and nondeterministic functional calculi we define a powerdomain functor Ρ such that it is an endofunctor over the category of algebraic lattices. Ρ is locally continuous and we study the initial solution D∞ of the domain equation D = Ρ([D → D]⊥). We derive from the algebras of Ρ the logic of D∞, that is the axiomatic description of its compact elements. We then define a λ-calculus and a type assignment system using the logic of D∞ as the related type theory. We prove that the filter model of this calculus, which is isomorphic to D∞, is fully abstract with respect to the observational Preorder of the λ-calculus.
Bi-models: Relational Versus Domain-theoretic Approaches
Authors: Bucciarelli Antonio
Published: December 2019

We introduce a technique based on logical relations, which, given two models M and N of a simply typed lambda-calculus L, allows us to construct a model M/N whose L-theory is a superset of both Th(M) and Th(N). By means of some examples, we show that classic bi-domain constructions lack this property, in general.
Modal Tableaux with Propagation Rules and Structural Rules
Authors: Castilho Marcos A. , del Cerro Luis Fariñas , Gasquet Olivier , Herzig Andreas
Published: December 2019

In this paper we generalize the existing tableau methods for modal logics. First of all, while usual modal tableaux are based on trees, our basic structures are rooted directed acyclic graphs (RDAG). This allows natural tableau rules for some modal logics that are difficult to capture in the usual way (such as those having an accessibility relation that is dense or confluent). Second, tableau rules rewrite patterns, which are (schemas of) parts of a RDAG. A particular case of these rules are the single-step rules recently proposed by Massacci. This allows in particular tableau rule presentations for K5, KD5, K45, KD45, and S5 that respect the subformula property. Third, we divide modal tableau rules into propagation rules and structural rules. Structural rules construct new edges and nodes (without adding formulas to nodes), while propagation rules add formulas to nodes. This distinction allows to prove completeness in a modular way.
Graded Consequence and Some Metalogical Notions Generalized
Authors: Chakraborty Mihir K. , Basu Sanjukta
Published: December 2019

The notion of graded consequence and some other metalogical notions like consistency, inconsistency, tautologihood and theoremhood to which grades have been introduced earlier by us are reviewed in the context of generalized operators. Some preliminary results regarding the relation between the notion of graded consequence and the notion of graded inconsistency are proved. The method of axiomatization is reconsidered in this general situation.
Transition-optimal Token Distribution
Authors: Chlebus Bogdan S. , Diks Krzysztof , Pelc Andrzej
Published: December 2019

There is given a graph, that models a communication network of a multiprocessor system, and there are tokens (jobs) allocated to nodes of the graph. The task is to distribute the tokens evenly, subject to the constraint that they may be moved only along the edges of the graph. The cost of a distribution strategy is measured as the total number of operations of moving a token along an edge. An algorithm for general graphs is developed, by reduction to a maximum-flow minimum-cost problem, that finds a cost-optimal distribution strategy, given a graph and an initial token allocation. The main result is an algorithm for graphs that are lines of nodes; it finds the distribution strategy in time O(n), for a line of n nodes.
Disjunctive Signed Logic Programs
Authors: Khamsi Mohamed A. , Misane Driss
Published: December 2019

In this work, we define signed disjunctive programs and investigate the existence of answer sets for this class of programs. Our main argument is based on an analogue of Tarski's fixed point theorem which we prove for multivalued mappings. This is an original approach compared to known techniques used to prove the existence of answer sets for disjunctive programs.
Jumping Petri Nets. Specific Properties
Authors: Ţiplea Ferucio Laurenţiu , Mäkinen Erkki
Published: December 2019

A Jumping Petri Net ([18], [12]), JPTN for short, is defined as a classical net which can spontaneously jump from a marking to another one. In [18] it has been shown that the reachability problem for JPTN's is undecidable, but it is decidable for finite JPTN's (FJPTN). In this paper we establish some specific properties and investigate the computational power of such nets, via the interleaving semantics. Thus, we show that the non-labelled JPTN's have the same computational power as the labelled or λ-labelled JPTN's. When final markings are considered, the power of JPTN's equals the power of Turing machines. The family of regular languages and the family of languages generated by JPTN's with finite state space are shown to be equal. Languages generated by FJPTN's can be represented in terms of regular languages and substitutions with classical Petri net languages. This characterization result leads to many important consequences, e.g. the recursiveness (context-sensitiveness, resp.) of languages generated by arbitrarily labelled (labelled, resp.) FJPTN's. A pumping lemma for nonterminal jumping net languages is also established. Finally, some comparisons between families of languages are given, and a connection between FJPTN's and a subclass of inhibitor nets is presented.
Automated Deduction Techniques for Studying Rough Algebras
Authors: Vigneron Laurent
Published: December 2019

We present a non-exhaustive state of the art in the domain of deduction in first-order logic with equality, describing different strategies introduced over the years: strategies for selecting deduction steps, for eliminating redundant information, for delaying the resolution of unsolved or too difficult problems, for applying deductions with built-in properties. We also present the system daΤac that implements our deduction techniques modulo associative-commutative properties. Finally we detail an application of those techniques to the study of non-classical logics, work realised in collaboration with Prof. Wasilewska (Stony Brook University, New York).
Computable Approximations of Reals: An Information-Theoretic Analysis
Authors: Calude Cristian S. , Hertling Peter H.
Published: December 2019

How fast can one approximate a real by a computable sequence of rationals? Rather surprisingly, we show that the answer to this question depends very much on the information content in the finite prefixes of the binary expansion of the real. Computable reals, whose binary expansions have a very low information content, can be approximated (very fast) with a computable convergence rate. Random reals, whose binary expansions contain very much information in their prefixes, can be approximated only very slowly by computable sequences of rationals (this is the case, for example, for Chaitin's Ω numbers) if they can be computably approximated at all. We also show that one can computably approximate any computable real very slowly, with a convergence rate slower than any computable function. However, there is still a large gap between computable reals and random reals: any computable sequence of rationals which converges (monotonically) to a random real converges slower than any computable sequence of rationals which converges (monotonically) to a computable real.
Powerdomain of Paths for Representing Object Structures
Authors: Pankowski Tadeusz
Published: December 2019

A new method for viewing and manipulating identity-based object structures is proposed. The method is founded on the viewing the object structure as an object graph which in turn is represented as a set of paths. Over a power set of paths we construct a powerdomain which forms a lattice with well-defined meet and join operations. In our construction of the powerdomain of paths we combine the Hoare ordering (appropriate for ordering of tuple objects) with the Smyth ordering (appropriate for ordering of set objects) into a new ordering appropriate for set of paths capturing information conveyed by both tuple and set objects. The approach allows to deal with incomplete tuple objects as well as with partially described sets. The goal of the powerdomain construction is to provide a semantic domain for a path calculus language [20], where path calculus variables range over paths and path calculus queries give sets of paths as their answers.
Termination of Graph Rewriting is Undecidable
Authors: Plump Detlef
Published: December 2019

It is shown that it is undecidable in general whether a graph rewriting system (in the “double pushout approach”) is terminating. The proof is by a reduction of the Post Correspondence Problem. It is also argued that there is no straightforward reduction of the halting problem for Turing machines or of the termination problem for string rewriting systems to the present problem.
Parameterized Structured Operational Semantics
Authors: Ferrari Gian Luigi , Montanari Ugo
Published: December 2019

A generalization of De Simone format, where labels of transitions are structured actions, is presented. This provides a parameterized SOS framework where several paradigms of the observational semantics of process calculi can be uniformly handled. Moreover, standard algebraic techniques provide the formal machineries to relate the different semantics. It is also shown that much of the meta results developed for standard SOS format extend to this parameterized context.
From Optimal Hyperplanes to Optimal Decision Trees
Authors: Son Nguyen Hung
Published: December 2019

We present an optimal hyperplane searching method for decision tables using Genetic Algorithms. This method can be used to construct a decision tree for a given decision table. We also present some properties of the set of hyperplanes determined by our methods and evaluate an upper bound on the depth of the constructed decision tree.
Adding Partial Orders to Linear Temporal Logic
Authors: Bhat Girish , Peled Doron
Published: December 2019

Modeling execution as partial orders increases the flexibility in reasoning about concurrent programs by allowing the use of alternative, equivalent execution sequences. This is a desirable feature in specifying concurrent systems which allows formalizing frequently used arguments such as ‘in an equivalent execution sequence’, or ‘in a consistent global state, not necessarily on the execution sequence’ to be formalized. However, due to the addition of structure to the model, verification of partial order properties is non-trivial and sparse. We present here a new approach which allows expressing and verifying partial order properties. It is based on modeling an execution as a linear sequence of global states, where each state is equipped with its past partial-order history. The temporal logic BPLTL (for Branching Past Linear Temporal Logic) is introduced. We provide a sound and relatively complete proof system for the logic BPLTL over transitions programs. Our proof system augments an existing proof system for LTL.
Processes of Contextual Nets and their Characteristics
Authors: Winkowski Józef
Published: December 2019

Generalized Place/Transition Petri nets, called contextual nets, and processes of such nets are considered. Processes of contextual nets are represented as partial orders with some extra structure. Operations of composing processes are defined such that each process of a contextual net can be obtained by combining processes corresponding to places and transitions of this net. Matrix-like characteristics of processes, called tables, and natural operations on such characteristics are defined such that the correspondence between processes and their characteristics is a homomorphism.
Remarks on Operations Suggested by Mutations in Genomes
Authors: Dassow Jürgen , Păunt Gheorghe
Published: December 2019

In the last years the operation of splicing which models a special type of recombination of genomes has been intensively studied, e.g. the effect of application of splicings to language families of classical formal language theory has been investigated. In this paper we present analogous results with respect to the operations inversion, translocation and duplication which are also descriptions of mutations of genomes.
Truth of Duration Calculus Formulae in Timed Frames
Authors: Middelburg Kees A.
Published: December 2019

Duration calculus is a logical formalism designed for expressing and refining real-time requirements for systems. Timed frames are essentially transition systems meant for modeling the time-dependent behaviour of programs. We investigate the interpretation of duration calculus formulae in timed frames. We elaborate this topic from different angles and show that they agree with each other. The resulting interpretation is expected to make it generally easier to establish semantic links between duration calculus and formalisms aimed at programming. Such semantic links are prerequisites for a solid underpinning of approaches to system development that cover requirement capture through coding using both duration calculus and some formalism(s) aimed at programming.
Pregrammars Versus Submonoids
Authors: Ostravský Jan
Published: December 2019

Prelanguages and pregrammars introduced in [8] present a generalization of languages and pure grammars. Relation of domination and double domination may be easily transferred from languages to prelanguages. In the present paper submonoids of a commutative monoid are characterized by means of their relations of domination; subgroups of a commutative group are characterized by means of their relations of double domination. The submonoid generated by a subset of a commutative monoid is constructed using a suitable pregrammar.
Simple and Minimal Ground Term Equation Systems
Authors: Vágvölgyi Sándor
Published: December 2019

A ground term equation system (gtes for short) E is simple if there is no gtes E′ equivalent to E consisting of less equations than E has. Moreover, a gtes E is minimal if for each equation e ∈ E, the congruence generated by E – {e} is a proper subset of the congruence generated by E. Given a reduced ground term rewriting system R, we describe all simple gtes' E and minimal gtes' F equivalent to R. We show that for a reduced ground term rewriting system R, it is decidable whether or not there exist infinitely many simple (minimal) gtes' equivalent to R. Finally, we show that for a reduced ground term rewriting system R, and a gtes E, it is decidable if there is a simple gtes F equivalent to R such that E ⊆ F.
Multi Lingual Sequent Calculus and Coherent Spaces
Authors: Jung Achim , Kegelmann Mathias , Moshier M. Andrew
Published: December 2019

We study a Gentzen style sequent calculus where the formulas on the left and right of the turnstile need not necessarily come from the same logical system. Such a sequent can be seen as a consequence between different domains of reasoning. We discuss the ingredients needed to set up the logic generalised in this fashion. The usual cut rule does not make sense for sequents which connect different logical systems because it mixes formulas from antecedent and succedent. We propose a different cut rule which addresses this problem. The new cut rule can be used as a basis for composition in a suitable category of logical systems. As it turns out, this category is equivalent to coherent spaces with certain relations between them. Finally, cut elimination in this set-up can be employed to provide a new explanation of the domain constructions in Samson Abramsky's Domain Theory in Logical Form.
Iteration Lemmata for Certain Classes of Word, Trace and Graph Languages
Authors: Kudlek Manfred
Published: December 2019

Using general iteration lemmata for languages defined by rational, linear, and algebraic systems of equations on ω-complete semirings, it can be shown that such iteration lemmata hold for certain classes of word and trace languages, and for process algebra classes related to them. The basic operation has to be associative with a neutral element, and is extended to sets of elements, such that the structure defined by it together with union and ∅ is an ω-complete semiring. With this property rational, linear and algebraic systems of equations can be defined, having a unique minimal solution as least fixed points. To guarantee iteration lemmata for the corresponding rational, linear and algebraic classes, a norm on the structure has to exist, fulfilling some monotonicity on union and extended operation on sets. This article is an extended version of the paper presented at the workshop CS&P'98 in Berlin, September 28-30, 1998.
On Causality Semantics of Nets with Priorities
Authors: Janicki Ryszard , Koutny Maciej
Published: December 2019

In the formal treatment of concurrent computing systems, causality and weak causality can be used to provide abstract specifications of the temporal ‘earlier than’ and ‘not later than’ orderings. In this paper we consider relational structures comprising causality and weak causality — called stratified order structures — which can be used to provide a non-sequential semantics of Petri nets with inhibitor arcs. We show that this approach can be extended to nets augmented with priority specifications. In particular, we demonstrate how to derive stratified order structures for such nets by generalising the standard construction of causal partial orders based on occurrence nets.
A Subtyping for Extensible, Incomplete Objects
Authors: Bono Viviana , Bugliesi Michele , Dezani-Ciancaglini Mariangiola , Liquori Luigi
Published: December 2019

We extend the type system for the Lambda Calculus of Objects [16] with a mechanism of width subtyping and a treatment of incomplete objects. The main novelties over previous work are the use of subtype-bounded quantification to capture a new and more direct rendering of MyType polymorphism, and a uniform treatment for other features that were accounted for via different systems in subsequent extensions [7, 6] of [16]. The new system provides for (i) appropriate type specialization of inherited methods, (ii) static detection of errors, (iii) width subtyping compatible with object extension, and (iv) sound typing for partially specified objects.
On the Relationships among four Timed Process Algebras
Authors: Corradini Flavio , D'Ortenzio Domenicantonio , Inverardi Paola
Published: December 2019

In this paper we contrast (the core of) four well-known process algebras specifically enriched for the specification and verification of timed systems. The aim of this comparison is twofold. On one hand it permits to gain confidence on how time and time passing are modelled in the four different timed process algebras. On the other hand, it establishes conditions under which mappings from a calculus to another can be provided which preserve (strong bisimulation-based) behavioural equivalence.
On Synchronization in P Systems
Authors: Păun Gheorghe , Yu Sheng
Published: December 2019

The P systems were recently introduced as distributed parallel computing models of a biochemical type. Multisets of objects are placed in a hierarchical structure of membranes and they evolve according to given rules, which are applied in a synchronous manner: at each step, all objects which can evolve, from all membranes, must evolve. We consider here the case when this restriction is removed. As expected, unsynchronized systems (even using catalysts) are weaker than the synchronized ones, providing that no priority relation among rules is considered. The power of P systems is not diminished when a priority is used and, moreover, the catalysts can change their states, among two possible states for each catalyst.
Thue Specifications and Their Monadic Second-order Properties
Authors: Knapik Teodor , Calbrix Hugues
Published: December 2019

This paper introduces oriented Thue specifications and their models which are simple directed edge-labeled graphs. The monadic second-order theory of these models is investigated and shown decidable for the class of suffix-bounded rational oriented Thue specifications. In addition, a characterization of prefix-closed context-free languages is given in terms of oriented Thue specifications.
An Assistant Agent
Authors: Müller Heike , Hilbrich Torsten , Kühnel Ralf
Published: December 2019

The paper describes an application of agent oriented programming: an assistant program for everyday computer tasks like printing, converting, extracting etc. The assistant looks for services matching the users query, possibly delegates queries to other agents, loads new services over the net and offers its own services to other agents. We use Java as implementing language.
Inductive Inference with Procrastination: Back to Definitions
Authors: Ambainis Andris , Freivalds Rūsiņš , Smith Carl H.
Published: December 2019

In this paper, we reconsider the definition of procrastinating learning machines. In the original definition of Freivalds and Smith [FS93], constructive ordinals are used to bound mindchanges. We investigate possibility of using arbitrary linearly ordered sets to bound mindchanges in similar way. It turns out that using certain ordered sets it is possible to define inductive inference types different from the previously known ones. We investigate properties of the new inductive inference types and compare them to other types.
Meta-Queries on Deductive Databases
Authors: Doherty Patrick , Kachniarz Jarosław , Szałas Andrzej
Published: December 2019

We introduce the notion of a meta-query on relational databases and a technique which can be used to represent and solve a number of interesting problems from the area of knowledge representation using logic. The technique is based on the use of quantifier elimination and may also be used to query relational databases using a declarative query language called SHQL (Semi-Horn Query Language), introduced in [6]. SHQL is a fragment of classical first-order predicate logic and allows us to define a query without supplying its explicit definition. All SHQL queries to the database can be processed in polynomial time (both on the size of the input query and the size of the database). We demonstrate the use of the technique in problem solving by structuring logical puzzles from the Knights and Knaves domain as SHQL meta-queries on relational databases. We also provide additional examples demonstrating the flexibility of the technique. We conclude with a description of a newly developed software tool, The Logic Engineer, which aids in the description of algorithms using transformation and reduction techniques such as those applied in the meta-querying approach.