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 _{1}* and

*F*are formulas, the following are also formulas:

_{2}*¬F*(negation), which is true if and only if

_{1}*F*is false;

_{1}*F*(conjunction), which is true if and only if both

_{1}∧ F_{2}*F*and

_{1}*F*are true;

_{2}*F*(disjunction), which is true if and only if

_{1}∨ F_{2}*F*or

_{1}*F*is true;

_{2}*F*(implication), which is true if and only if

_{1}⇒ F_{2}*F*is false or

_{1}*F*is true;

_{2}*F*(equivalence), which is true if and only if

_{1}⇔ F_{2}*F*and

_{1}*F*have the same truth value; ∀

_{2}`x`

*F*(universal quantification), which is true if and only if

_{1}*F*is true for every object

_{1}`x`in the domain; and ∃

`x`

*F*(existential quantification), which is true if and only if

_{1}*F*is true for at least one object

_{1}`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.