If-and-only-if expresses biconditional logical connective between two statements. The statements should contain X/Y variables. It is used for making axioms on properties/roles (such as have-child or have-sibling).


Those examples show how make axioms on properties

Example: has-child is reverse of has-parent.
X has-child Y if-and-only-if Y has-parent X.
Example: has-sibling is symmetric.
X has-sibling Y if-and-only-if Y has-sibling X.