3.4 Performance of Automated Reasoners 59
Summary
- Theorem provers prove theorems.
- Queries to a theorem-proving system are expressed as conjectures.
- Theorem proving is very difficult, so numerous strategies have been de-
veloped.
- Specialized theorem provers limit the kind of theory so as to improve per-
formance:
- Constraint solvers
- Description logic
- Business rule systems
3.4 Performance of Automated Reasoners
Any particular reasoning operation (whether it is an inference or a query) is
always performed within a fixed, known context. If the reasoning context
(also known as the knowledge base) changes over time, then steps must be
taken to ensure that the operation is not affected by the changes. This is the
same as query processing in a relational database which uses transactions
(most commonly implemented by using a locking mechanism) to ensure that
updates do not interfere with the results. Because it can be inefficient for
each query to be performed by scanning all of the data, relational databases
usually maintain indexes on the data. However, there is a cost, both in time
and in storage space, to maintain the indexes. An index is useful only if
the cost of maintaining the index is compensated by the improvement in
performance that it provides. If most uses of the database require examining
most of the data, then an index should not be maintained.
A similar situation occurs in automated reasoners. Specialized indexing
structures, such as the Rete network maintained by a Rete engine, requires
additional computer time and storage space to maintain. This overhead must
be compensated by an improvement in performance for the indexing struc-
ture to be worthwhile. The way that the knowledge base is used will de-
termine whether the Rete network provides an overall improvement in per-
formance. Generally speaking, the theorem provers (including description
logic systems) are suitable primarily for static knowledge bases. Backward
chainers and non-Rete forward chainers are intermediate. They have some
