Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

Predicate Calculus

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., f(a,b,x) ). Atomic sentences are formed by applying a predicate to a set argument term (e.g., P(f(a,b,x),c,g(h(y)) ). Compound sentences are formed by adding negation to a sentence (e.g., ¬ R(a,b) ), 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:

(x)Q(x): `for all x, Q(x)'

and existential statements:

(z)R(z,a): `there exists a z such that R(z,a)'

Automatic inference techniques (e.g., Resolution) for first-order logic have been widely explored.



Add Comment

No comments.