Existential Quantifiers in Predicate-Fact-Nets
It is well known that every formula of first-order predicate logic in prenex form can be represented as a strict predicate transition net (PrT-net) in which all transitions are seen to be dead. Nets wherein all predicates can carry only one specimen of an n-tuple are called strict [Ge]. In this net representation of predicate logic Skolem functions are used to get descriptions for existential quantifiers [Th].
In PrT-systems given by PrT-nets and an initial marking, the dead transitions specify the facts about that system. S-invariants are a very useful means to prove transitions of a PrT-system to be facts. In those predicate fact nets (PrF-nets) derived from S-invariants, Skolem functions do not occur.
The question arises, whether existential quantifiers do not exist in those fact nets, or whether nets carry another more natural representation for them. Sums seem to yield such an appropriate net description for existential quantifiers. But some derivation problems remain, in which sums cannot replace the Skolem functions.
KeywordsPredicate Logic Existential Quantifier Derivation Problem Skolem Function Resolution Rule
Unable to display preview. Download preview PDF.
- [Ge]H.J. Genrich Projections of CE-Systems Proc. of 6th European Workshop on Application and Theory of Petri Nets Espoo, Finland 1985Google Scholar
- [GLT]H.J. Genrich; K. Lautenbach; P. Thiagarajan Elements of General Net Theory in: W. Brauer (Ed.) Net Theory and Applications Springer-Verlag 1980Google Scholar
- [GT]H.J. Genrich; G. Thieler-Mevissen The Calculus of Facts in: A. Mazurkiewicz (Ed.) Math. Foundations of Computer Science 1976 Lecture Notes in Computer Science Vol. 45 Springer-Verlag 1980Google Scholar
- [Th]G. Thieler-Mevissen The Petri Net Calculus of Predicate Logic Internal Report GMD-ISF 76-09Google Scholar