The reachability problem for Petri nets and decision problems for Skolem arithmetic
1980; Elsevier BV; Volume: 11; Issue: 2 Linguagem: Inglês
10.1016/0304-3975(80)90042-0
ISSN1879-2294
AutoresEgon Börger, Hans Kleine Büning,
Tópico(s)Logic, Reasoning, and Knowledge
ResumoWe show that the decision problem for the class C0 of all closed universal Horn formulae in prenex conjunctive normal form of extended Skolem arithmetic without equality (i.e. first order formulae built up from the multiplication sign, constants for the natural numbers and free occuring predicate symbols) is exponentially time bounded equivalent to the reachability problem for Petri nets if restricted to the class of formulae with (a) only monadic predicate symbols, with (b) only binary disjunctions in the quantifier free matrix and (c) without terms containing a variable more than once. We show that leaving out one of the restrictions (a) to (c) yields classes of formulae whose decision problem can assume any prescribed recursively enumerable complexity in terms of many-one degrees of unsolvability.
Referência(s)