Catalogue of Artificial Intelligence Techniques
Aliases: First-order Logic, Predicate Logic
Keywords: axioms, connective, inference rules, quantifiers, terms, theorem
Categories: Knowledge Representation
Author(s): Graeme Ritchie
Predicate calculus is a formal language in which it is possible to express statements about simple domains. It comprises a set of symbols, and rules for combining these into terms and formulae. There are also rules of inference, which state how a new formula can be derived from old formulae. A logical system will have an initial set of sentences (`axioms') and any sentence which can be derived from these axioms using the inference rules is called a `theorem' of the system. The standard logic is a well-defined notation in which exact descriptive statements can be formulated about any `model' (i.e., set of objects with relations between them). Moreover, purely formal manipulations of these symbolic statements (i.e., inference) can be used to produce further valid descriptions of that same model, without direct reference to the model itself. Terms can be constants (names of objects), variables (marking which part of a formula is quantified) or functions applied to arguments (e.g., ). Atomic sentences are formed by applying a predicate to a set argument term (e.g., ). Compound sentences are formed by adding negation to a sentence (e.g., R ), joining two statements with a connective such as (`and'),
(`or'), (`implication'). There are two quantifiers which, used together with variables, allow the expression of universal statements:
and existential statements:
Automatic inference techniques (e.g., Resolution) for first-order logic have been widely explored.
- Crossley, J.N. et. al., What is Mathematical Logic?
, Oxford University Press, Oxford, 1972.