Formal Methods and Semantics

There is one other way to represent semantics, called "formal methods." Formal methods have two primary advantages:

• They can be reasoned about with mathematical precision. Truth can be deduced and proven, based on a set of assertions and rules of logic.

• They can be more easily, reliably, and predictably translated to machine-executable instructions. This means that if you can express your semantics completely in formal terms, translating them to executable systems is usually straightforward.

Formal methods have two downsides:

• Few people are comfortable reading or writing formal descriptions. They glaze over when they even look at them.

• They don't scale very well. They rely on human retention of a large number of semantics expressed in Greek symbols, and after a few dozen assertions many people cannot assimilate any more.

Some tools, such as OilEd,^[71] allow the construction of an ontology graphically and then convert it to formal notation.

We'll discuss formal semantics briefly. I have not done any work with them, but found in the research for this book that many good sources of semantic insight use these notations extensively. I've assembled a brief "decoder ring" (Figure 10.14) that you can use if you find yourself faced with a semantics book with many non-English characters in it.

Symbol	Read as	Official Name	Means
∃ ∃!	There exists … There is exactly one …	Existential Quantifier Exactly One Quantifier	There is at least one … There is one and only one …
∃!!	There is one unique	Unique Existential Quantifier	There is a one to one relationship between the two things noted
∀	For every …	Universal Quantifier	This is what is true for all things of this type
⊃	If … then …	Material Implication	if x is true then y must be true, but no implication if x is not true
∧	And	Conjunction	And
∨	Or	Disjunction	Or
|	Either	Exclusive Or	XOR
≍	If and only if	Equivalence	Two expressions represent the same thing
∈	Is a member of	Set	Is in the set
@	Count	Count	Count
~ ⊧	Not … implies …	Negotiation Semantic Entailment	Not the second statement is inferable from the first within a particular context
⊢	… is provable from	Provability	second statement can be proven from the first without contextual information
∩	… intersect …	Intersection	everything that is part of a and b
∪	… union …	union	everything that is part of a and b

Figure 10.14: The formal semantics "decoder ring."

If you find yourself getting more involved with this you may want to consider John Sowa's Knowledge Representation: Logical, Philosophical and Computational Foundations^[72] or Richard Epstein's The Semantic Foundations of Logic .^[73]

This allows us to make assertions about the problem domain such as the one shown in Figure 10.15. The graphical description is equivalent to the formal notation underneath (this example uses the notation as per John Sowa's Knowledge Representation^[74]). Read Figure 10.15 as "for every sculpture (x) there exists a location (y) such that (x) is ‘at’ (y)" or "every sculpture has a location."

Figure 10.15: Each sculpture is in a location.

Obviously, this is a simple example. However, these systems can become extremely complex, and the challenge is in reasoning about these complex structures.

^[71]See http://oiled.man.ac.uk/ for further information.

^[72]John F. Sowa, Knowledge Representation: Logical, Philosophical, and Computational Foundations. Pacific Grove: Brooks/Cole, 2000.

^[73]Richard L. Epstein, The Semantic Foundations of Logic: Predicate Logic. Oxford: Oxford University Press, 1994.

^[74]See Sowa, p. 477, for a similar example.