When I started working on and eventually writing about logic-based agents, I always remember having had some difficulty describing the logic formalism in a way that is informative and yet reads well. I have found a very concise and yet correct description of this terminology reading a paper from Pedro Domingos on Markov Logics. This description turns out to read so well that he has used it verbatim in almost a dozen papers and book chapters. So I took the liberty to adapt this description for my website in the section below. Notice that, unlike Prolog, the convention used in this description is that constants are represented as strings starting with an uppercase letter whereas variables are represented as strings starting with a lowercase letter.

First-order logic

A first-order knowledge base (KB) is a set of sentences or formulas in first-order logic. Formulas in first-order logic (FOL) are constructed using four types of symbols: constants, variables, functions, and predicates. Constant symbols represent objects in the domain of interest (e.g., people: Anna, Bob, Chris, etc.). Variable symbols range over the objects in the domain. Function symbols (e.g., MotherOf) represent mappings from tuples of objects to objects. Predicate symbols represent relations among objects in the domain (e.g., Friends) or attributes of objects (e.g., Smokes). An interpretation specifies which objects, functions and relations in the domain are represented by which symbols. Variables and constants may be typed, in which case variables range only over objects of the corresponding type, and constants can only represent objects of the corresponding type. For example, the variable x might range over people (e.g., Anna, Bob, etc.), and the constant C might represent a city (e.g, Seattle, Tokyo, etc.).

A term is any expression representing an object in the domain. It can be a constant, a variable, or a function applied to a tuple of terms. For example, Anna, x, and GreatestCommonDivisor(x, y) are terms. An atomic formula or atom is a predicate symbol applied to a tuple of terms (e.g., Friends(x, MotherOf(Anna))). Formulas are recursively constructed from atomic formulas using logical connectives and quantifiers. If F₁ and F₂ are formulas, the following are also formulas: ¬F₁ (negation), which is true if and only if F₁ is false; F₁ ∧ F₂ (conjunction), which is true if and only if both F₁ and F₂ are true; F₁ ∨ F₂ (disjunction), which is true if and only if F₁ or F₂ is true; F₁ ⇒ F₂ (implication), which is true if and only if F₁ is false or F₂ is true; F₁ ⇔ F₂ (equivalence), which is true if and only if F₁ and F₂ have the same truth value; ∀x F₁ (universal quantification), which is true if and only if F₁ is true for every object x in the domain; and ∃x F₁ (existential quantification), which is true if and only if F₁ is true for at least one object x in the domain. Parentheses may be used to enforce precedence. A positive literal is an atomic formula; a negative literal is a negated atomic formula. The formulas in a KB are implicitly conjoined, and thus a KB can be viewed as a single large formula. A ground term is a term containing no variables. A ground atom or ground predicate is an atomic formula all of whose arguments are ground terms. A possible world (along with an interpretation) assigns a truth value to each possible ground atom.

A formula is satisfiable if and only if there exists at least one world in which it is true. The basic inference problem in first-order logic is to determine whether a knowledge base KB entails a formula F, i.e., if F is true in all worlds where KB is true (denoted by KB ⊨ F ). This is often done by refutation: KB entails F if and only if KB ∪ ¬F is unsatisfiable. (Thus, if a KB contains a contradiction, all formulas trivially follow from it, which makes painstaking knowledge engineering a necessity.) For automated inference, it is often convenient to convert formulas to a more regular form, typically clausal form (also known as conjunctive normal form (CNF)). A KB in clausal form is a conjunction of clauses, a clause being a disjunction of literals. Every KB in first-order logic can be converted to clausal form using a mechanical sequence of steps. Clausal form is used in resolution, a sound and refutation-complete inference procedure for first-order logic.