ATMS vs. JTMS
Main differences come from:
way to store logical dependencies
For a node n, JTMS stores only the assertions which directly imply n.
For a node n, ATMS stores the set(s) of assumptions (the environment) which imply n.
information made visible by the ATMS to the PS
JTMS provides one context at the time. JTMS chooses one context and forces the PS to work on it.
ATMS provides all contexts (possibly inconsistent among them) and lets the PS choose the most adequate one.