What does semicommutative mean? I'm reading J. A. Robinson's A Machine-Oriented Logic Based on the Resolution Principle, and have hit a word I don't know: semicommutative. He says:
"An informal grasp of the general notion of resolution is obtainable now, prior to its exact treatment, from simply contemplating the fundamental property which it will be shown to possess: resolution is semicommutative with saturation." He explains further: "If $S$ is any set of clauses, and $P$ is any subset of the Herbrand universe of $S$, then: $\mathbb{R}(P(S)) \subseteq P(\mathbb{R}(S))$."
I'm used to the equational/algebraic formulation of commutativity: $x \cdot y = y \cdot x$. I can see the similarity with Robinson's equation, and that an improper subset is in some sense "less" than equality and therefore might give rise to "semi", but I haven't been able to formalize what the definition of semicommutative in my mind.
 A: 
I haven't been able to formalize what the definition of semicommutative in my mind.

You shouldn't have to do that.  It would be worth checking some of the references to see if it was consistently used by contemporary articles.
By adding "semi", it just means that the two are not completely commutative. In this case, the composition in different orders results in two sets that are not equal, but at least related by containment in one way.
It could be that this is not standard terminology. To give you an example of other uses I've turned up:


*

*In ring theory, a semicommutative ring is one in which $ab=0$ implies $arb=0$ for every $r$ in the ring

*Another one I saw is that $f,g$ are semicommutative if some sort of commutator $[f,g]$ is in a certain class. (this appears to be the usage for differential operators.)

*Here's another one that I won't pretend to understand.

*Here is another one from algebra where it means that $fg=cgf$ for some nonzero constant.
From the context here, it looks like $f,g$ are functions on a poset $X$, and that $f$ semicommutes with $g$ if $f\circ g\subseteq g\circ f$.
