axioms of PSL are organized into PSL-Core and a set of extensions.
PSL-Core is the set of axioms written in CLIF (the Common
Logic Interchange Format) and using only the nonlogical lexicon of
PSL-Core. The extensions form a lattice of extensions to PSL-Core.
The purpose of PSL-Core is to axiomatise a set of intuitive semantic primitives that is
adequate for describing the fundamental concepts of manufacturing processes.
Consequently, this characterization of basic processes makes few assumptions about their
nature beyond what is needed for describing those processes, and the Core is therefore
rather weak in terms of logical expressiveness.
In particular, PSL-Core is not strong enough to provide definitions of the many
auxiliary notions that become necessary to describe all intuitions about manufacturing
To supplement the concepts of PSL-Core, the ontology includes a set of
extensions that introduce new terminology. An PSL extension provides the
logical expressiveness to express information involving concepts that
are not explicitly specified in PSL-Core. For each symbol in the
nonlogical lexicon of an extension of PSL, there exist one or more
axioms, written in CLIF, that constrain its interpretation. A
distinction is drawn between definitional and nondefinitional extensions
of PSL-Core. A definitional extension is an extension whose nonlogical
lexicon can be completely defined in terms of PSL-Core. Definitional
extensions add no new expressive power to PSL-Core. Nondefinitional
extensions (also called core theories) are extensions of PSL-Core that
involve at least one new primitive not contained in PSL-Core. All
extensions within PSL must be consistent extensions of PSL-Core, and may
be consistent extensions of other PSL extensions. However, not all
extensions within PSL need be mutually consistent.
The organization of the extensions below reflects the Parts within
18629. All files are updates to the standard,
except for those marked by “x”, which are in progress.
Other status indicators are: “c” (consistency proof
completed) and “ca” (consistency verified by the automated
theorem prover Vampire).
The syntax of all files has been checked by automated theorem provers, see
Duration and Ordering Theories
Embedded Activity Trees
Temporal and State Extensions
Embedded Activity Trees
Activity Ordering and Duration Extensions
Subactivity Occurrence Orderings
Processor Activity Extensions