Changes from PSL 2.0

General Comments

1. The axioms use the latest version of Common Logic (http://cl.tamu.edu), which no longer contains the defrelation or deffunction constructs. All definitions have been rewritten without this construct. Note that this change is only syntactic sugar; the old and new definitions are logically equivalent.

Part 12

occtree.th

1. To enhance readability, the axioms for earlier were moved to the beginning of the file, so that the numbering of the axioms has been changed.
2. The old Axiom 2 (which stated that the successor function is a one-to-one mapping of activity occurrences to activity occurrences), has been replaced by a new Axiom 4, which states that a branch in the occurrence tree is totally ordered. This new axiom is stronger than the old one.

disc_state.th

1. Axiom 5 mistakenly referred to successor as a relation; this has been fixed.
2. The old Axiom 6 (Intertia Principle) has been replaced by two new axioms. This was necessary to prevent unintended models in which nonstandard branches of occurrence trees were dense rather than discrete.

subactivity.th

atomic.th

complex.th

1. Two new defined relations (sibling, cousin) have been introduced, which are used in later core theories and definitional extensions.
2. A new Axiom 9 has been added to guarantee that activity trees are discrete; the old axioms allowed nonstandard models with dense activity trees.
3. The old Axiom 8 (which stated that the min_precedes relation is transitive has been replaced by two Axioms 10 and 11, which are stronger than the old axiom.

act_occ.th

1. An activity argument has been added to the hom and mono relations, so that the mappings are restricted to trees for the same activity.
2. The root_occ relation has been changed to a function. This was originally a functional relation (since every activity occurrence has a unique root occurrence), and making it a function simplifies axioms and definitions elsewhere.
3. A new defined relation sibling has been introduced.
4. The same_tree relation has been renamed as same_grove since it may apply to multiple activity trees whose roots are siblings. The definition has been changed by the introduction of the new sibling relation.
5. The branch_mono relation has been removed.

Part 13

soo.th

1. A new primitive relation soo has been introduced and the relation parallel has been eliminated.

duration.th

1. Typos related to old versions of KIF have been corrected.

iterate.th

1. <_rep has been renamed as rep_precedes
2. References to same_tree have been replaced by the relation same_grove.
3. This extension was incorrectly using <_min instead of min_precedes; this typo has been fixed.

envelope.th

preserve.th

Part 41

ordered.def

1. The definitions of mono_tree and root_automorphic have been revised. These changes led to minor modifications to the class definitions in the remainder of the extension.
2. A new relation, order_tree has been introduced, which is necessary for the revised definition of root_automorphic.

permute.def

1. The definition of branch_monomorphic has been modified to incorporate the new version of mono, Also, this relation is no longer restricted to activity occurrences that are in the same grove.
2. References to same_tree have been replaced by the relation same_grove.

folded.def

1. The same_tree relation has been replaced by same_grove in all definitions.
2. The definition of branch_homomorphic has been fixed (the old definition incorrectly used the hom relation.

repetitive.def

1. The relation branch_mono (formerly found in acticc.th) has been revised and introduced into this extension, where it is needed for the class definitions.

branchwise.def

1. The definitions incorrectly used activity arguments in branch_automorphic and same_tree; these errors have been fixed.
2. The same_tree relation has been replaced by same_grove in all definitions.

compacted.def

1. The definitions incorrectly used activity arguments in branch_homomorphic and same_tree; these errors have been fixed.
2. The same_tree relation has been replaced by same_grove in all definitions.

treeordered.def

1. The definitions incorrectly used atomic subactivity arguments in root_automorphic; these errors have been fixed.
2. The same_tree relation has been replaced by same_grove in all definitions.

subtree.def

1. The header information incorrectly stated that this extension required variation.def. The subtree.def extension does not depend on any other definitional extension.
2. Since all of the activity occurrence arguments in the definitions refer to atomic activity occurrences, ?occ variables were renamed as ?s variables.
3. The definition of subtree_embed has been tightened.

embedding.def

1. This extension was incorrectly using <_min instead of min_precedes; this typo has been fixed.

Part 42

Part 43

strongposets.def

This extension has been replaced by a completely new one.

weakposets.def

This extension been temporarily removed; it will be replaced by a new one in the next release.

iterate.def

1. The same_tree relation has been replaced by same_grove in all definitions.
2. <_rep has been renamed as rep_precedes
3. Typos related to old versions of KIF have been corrected.

Parts 14, 44, 45, 46