This chapter is the deck M9 — Automated Reasoning, the second half of the logic arc that Chapter 8 opened. The deck itself carries a rare disclaimer: it is “mostly derived — somewhere quite straightforwardly” from a very good, short, and clear paper on automated reasoning [Bonacina and Martelli, 2006], published in the special issue of Intelligenza Artificiale celebrating the first fifty years of AI. Every problem or mistake in the slides belongs to the deck’s author; the good ideas, the paper’s. The chapter has two halves: sections 1 to 11 are automated reasoning in classical logic; sections 12 to 20 move to non-classical logics, extensions of logic programming, model checking, and applications. Chapter 10 will keep the search machinery and change the object: from proofs to plans.
The deck opens by stating the central problem in automated reasoning in one sentence, and it is worth memorising because the whole chapter is a commentary on it: determining whether a conjecture φ, that represents a property to be verified, is a logical consequence of a set S of assumptions, which express properties of the object of study — e.g., a system, a circuit, a program, a data type, a communication protocol, a mathematical structure.
So the problem has two ingredients. A conjecture φ: a property we wish to verify. And a set of assumptions S: properties of the object of study. And the question connecting them is the entailment question of Chapter 8, S |= φ, now asked of a machine: is φ true in every interpretation making all formulas of S true?
Then the deck immediately adds the conjoint problem: knowledge representation. The entailment question cannot even be posed until we have suitable formalisms for S and φ — formalisms able to represent aspects of the real world such as action, space, time, mental events, and commonsense reasoning. The two problems are inseparable: the choice of representation determines what can be expressed, and expressiveness determines what can be reasoned about.
Given the conjoint problem, which logics are actually used to represent knowledge? The deck’s answer is a two-part list that sets up the whole chapter:
This is the same duality Chapter 8 met from the theory side: classical logic is where the proof machinery lives, but the aspects of the real world listed above — action, space, time, mental events — do not sit naturally inside it. So the field splits: either extend classical logic with new connectives and new proof techniques, or keep classical logic and find translations. Both strategies appear in this chapter.
Determining whether a conjecture φ is a logical consequence of a set S of assumptions is a matter of theorem proving: that is, finding a proof of φ from S. The deck then draws two dichotomies that organise the whole field.
The distinction matters because the two problems have completely different computational behaviour, as the next section will make precise: one is semi-decidable, the other is not even that.
These two axes are not aligned. It is perfectly possible to do deductive theorem proving interactively, and in practice the harder classes — induction, model generation, higher-order reasoning — force interaction, exactly as section 5 will conclude.
How do theorem provers actually work? The deck’s answer is a surprise only to those who skipped Chapter 8:
The vast majority of theorem-proving methods work refutationally — that is, they prove that φ follows logically from S by showing that S ∪ {¬φ} generates a contradiction, or, is inconsistent.
Chapter 8 already met the canonical instance: SLD resolution in logic programming [Robinson, 1965]. It proves an atom G by showing that the program together with the negation of G — the goal ← G — is unsatisfiable. Same pattern, one level up: the whole entailment problem is solved by contradiction.
The other negative technique is automated model building [Caferra et al., 2004]: given assumptions S and conjecture φ, instead of trying to prove φ, try to disprove it by finding a counter-example or counter-model — that is, a model of S ∪ {¬φ}. If such a model exists, then φ is not a logical consequence of S, and the answer is no, with a witness.
Can a machine always settle S |= φ? The deck’s answer is the classical tri-partition of computability, and it is worth stating precisely:
And there is a practical consequence that the deck draws immediately:
Fully automated theorem proving focuses on deductive theorem proving; induction, model generation, and reasoning in higher-order logics resort to a larger extent to interactive theorem proving.
This is the chapter’s first appearance of the theme Chapter 6 found historically: the machine needs help exactly where the search space is worst. Semi-decidability says: if the proof exists, a machine can find it — but it gives no bound on how long the machine may search when it does not.
The deck now makes semi-decidability operational. A semi-decision procedure for the problem S |= φ behaves as follows:
Notice the asymmetry, which is the entire content of semi-decidability: yes is always eventually certified, no is never certified — only sometimes discovered, when the procedure happens to stop without a proof. And when it stops without a proof, the output may still be useful: it may contain enough structure to build a model of S ∪ {¬φ}, which is exactly the counter-model that automated model building of section 4 is after.
Why is this the best we can do? The deck’s answer is a matter of search space:
This is the exact same problem Chapter 6 recorded historically: the way out of the search explosion is not more speed, but knowledge and heuristics to prune the space. Here the same insight takes a computational form: the search plan (section 9) is the automation of that pruning.
The theorem-proving problem is not “find a proof” but “find a proof in a huge, mostly irrelevant search space”. Everything that follows — contraction rules, SAT solving, search plans, interactive proving — is a strategy for shrinking the space the machine actually explores. Chapter 6’s historical lesson and this chapter’s technical machinery are the same discovery.
Given the infinite search space, a prover that only generated consequences would drown in them. The deck’s key methodological point:
The ability to detect and discard redundant formulae is as crucial as the ability to generate consequences of given formulae.
Contemporary inference systems therefore feature both kinds of rule, and the deck gives the precise soundness conditions for each:
From these, the whole-system properties:
Rules that add formulae: what is generated is a logical consequence of the premises. Examples: resolution, paramodulation. Expansion grows the search space — it is how new theorems are discovered at all.
Rules that delete or simplify already-inferred theorems: what is removed is a logical consequence of what is left or added. Examples: subsumption, equational simplification. Contraction shrinks the search space — it is how redundancy is discarded. The deck’s point: both are equally crucial.
An inference system is sound if all its rules are sound — every expansion step generates consequences, every contraction step removes only consequences. Soundness is what keeps the system from proving false things.
The completeness property that matters for refutational theorem proving: if the initial set is inconsistent, the system must be able to derive a contradiction. Without it, a prover may fail to find a proof that exists.
Before the search-space problems of section 6, the deck reminds us that decidable instances of reasoning problems do exist: for these problems, the search space is finite and decision procedures are known. Decidability may stem from imposing restrictions on three different things:
And the most prominent instance of the first case is propositional logic itself, whose decidable satisfiability problem is known as SAT [Franco and Martin, 2009]. The deck underlines the practical significance: many problems in computer science can be encoded in propositional logic, reduced to SAT and submitted to SAT solvers — e.g., bounded model checking (BMC) [Biere et al., 2003].
As far as automated reasoning is concerned primarily with complete SAT solvers, the dominating approach is the DPLL (Davis–Putnam–Logemann–Loveland) algorithm [Davis et al., 1962] — a depth-first search with unit propagation, pure-literal elimination and backtracking. It is a striking instance of the chapter’s theme: a decision procedure is still a search procedure, just one with a finite space and a known termination guarantee.
And here the deck inserts the warning that ties section 8 to section 6:
Decidable does not mean computationally tractable: decidable reasoning problems are typically NP-complete. Overall, automated reasoning problems range from decidable (but NP-complete) to semi-decidable, or not even semi-decidable. This is why automated reasoning relies almost universally on the AI paradigm of search.
Now the deck states the conceptual core of the whole chapter:
Automated reasoning methods are strategies, composed of an inference system and a search plan.
And the one-line summary worth memorising:
It is the addition of the search plan that turns a non-deterministic inference system into a deterministic proof procedure.
Notice how precisely this maps onto Chapter 8. There, SLD resolution was the inference rule and the left-to-right, top-to-bottom, depth-first strategy was the search plan; Prolog was the deterministic proof procedure they made together. Here the pair is generalised: the same two ingredients compose every automated reasoning method.
The deck lists, just to mention them, the main families of strategies in the literature: ordering-based vs. contraction-based strategies; semantic strategies; subgoal reduction strategies; instance-based strategies. You are not expected to know their mechanics, but you are expected to recognise the pattern: every one of them is a way to decide, among all the inferences the inference system permits, which ones to actually perform.
Section 5 said that induction, model generation and higher-order reasoning resort to a larger extent to interactive theorem proving. Here the deck makes that precise. Interactive reasoning systems with higher-order features also employ search, but only indirectly, or at the meta-level — because the search is made of both automated and human-driven steps:
This is where the chapter’s theme meets Chapter 6’s lesson head-on: the human supplies the knowledge — the lemmas, the strategic choices, the decomposition into subproblems — that the machine cannot discover on its own, and the machine supplies the mechanical search the human cannot sustain. Neither alone would be enough.
“In spite of all the issues and complexity”, the deck says, automated reasoning has relevant — even essential — applications. The list is worth keeping as a map of where the machinery actually pays:
The point of the list, from the course’s standpoint: automated reasoning is not a laboratory curiosity. It is the shared engine under verification (Chapter 4’s agents, Chapter 7’s BDI), declarative programming (Chapter 8), and — as the next sections show — planning, agent programming and the web.
The second half of the deck moves to the non-classical side. The starting observation: many aspects of AI problems can be modelled with logical formalisms — yet many of them with the so-called non-classical logics [Morgan, 1976], e.g., modal logics and temporal logics. These logics add machinery that classical FOL lacks: modalities for necessity and possibility, temporal operators for time, and so on.
How does automated reasoning cope? The deck gives two complementary strategies:
The translation strategy is the technical heart of the second half: it is how the classical machinery of sections 1–11 stays useful even where the knowledge is irreducibly non-classical.
Add operators for necessity (□) and possibility (⋄); knowledge and belief (epistemic logic) are modal logics. Semantics is based on possible worlds and accessibility relations between them. Section 18 uses modal logic to represent actions.
Add operators for time: always, eventually, next, until. Properties have to do with the evolution of behaviour over time, so temporal logic is the standard language of model checking (section 17).
Fragments of first-order logic with decidable reasoning, designed for concept hierarchies and ontologies. They are the formal basis of OWL, the Semantic Web ontology language (section 20).
Logics where adding new information can retract old conclusions — the formal home of commonsense reasoning and revisable inferences (section 13).
Why do we need nonmonotonic logics at all? The deck’s answer connects to a historically-important research problem in AI: the logical formalisation of commonsense reasoning.
Traditional logics, even non-classical ones, are not suitable to express revisable inferences, which are instead the conceptual scope of nonmonotonic logics for nonmonotonic reasoning [Hanks and McDermott, 1986].
The key word is revisable. Classical logic is monotonic: if φ follows from S, it still follows from any superset of S — adding assumptions never removes conclusions. Commonsense reasoning is not like that: “birds fly” + “Tweety is a bird” gives “Tweety flies”, but adding “Tweety is a penguin” takes it back. Nonmonotonic logics make that retraction formal.
From the course’s perspective this matters twice over: it is the logical face of what Chapter 7 called belief revision in BDI agents, and it is the exact behaviour that negation as failure (section 14) and answer set programming (section 15) implement computationally.
Logic programming (LP) was proposed with the goal of combining the use of logic as a representation language with efficient deduction techniques based on a backward inference process (goal-directed), which allows a set of formulas (Horn clauses) to be considered as a program. Prolog is the most widely used logic programming language. While originally logic programming was conceived as a subset of classical logic, it was soon subject to non-classical extensions.
The first such extension is negation as failure (NAF) [Clark, 1978]:
In order to prove a negated goal ¬G, Prolog tries to prove G: if G cannot be proved, then the goal ¬G succeeds, and vice versa.
This simple feature has been widely used to achieve nonmonotonic behaviour. The deck’s observation is precise: by adding new formulas, a previously not-provable goal G might become true — and, as a consequence, ¬G might become false. That is exactly the nonmonotonicity of section 13, obtained operationally.
The semantics of NAF has been deeply studied, and the relations with nonmonotonic logics have been pointed out. The most widely accepted semantics is the answer set semantics [Gelfond, 2008]: according to this semantics, a logic program may have several alternative models, called answer sets, each corresponding to a possible view of the world.
Logic programming has been made more expressive by extending it with the so-called classical negation — that is, the monotonic negation of classical logic — and with disjunction in the head of rules. More recently, a new approach to handle negation has emerged: answer set programming (ASP) [Lifschitz, 2008].
Syntactically, ASP programs look like Prolog programs; the computational mechanisms used in ASP are different — more like SAT solvers. The idea is that an ASP computation results in 0, 1, or n sets of propositions (or formulas) justified by the program.
Notice the continuity with section 8: the ASP machinery is SAT-based, so the decision procedures of classical logic return as the engine of a non-classical programming paradigm. And notice the discontinuity with Prolog: a Prolog query has one computed answer at a time; an ASP computation returns all the justified sets at once.
high_salary <- employed, educated.
educated <- high_salary.
employed <- motivated.
motivated <-.The set {motivated, employed} is the only one justified, since neither high_salary nor educated can be derived from the program: they only support each other in a loop, with no ground support from any fact.
open <- not closed.
closed <- not open.The set {open} can be justified, by assuming closed will not be derived; at the same time, the set {closed} can be justified, by assuming open will not be derived. So the answer sets for the program above are {open} and {closed} — two possible worlds described by the program, as an example of nonmonotonic reasoning.
The two examples are asked constantly, and the contrast is the point. Example 1 has no negation: the loop high_salary ↔ educated is grounded nowhere, so it contributes nothing — one answer set, {motivated, employed}. Example 2 has negation as failure in both rules: each rule’s body is the negation of the other’s head, so there are two answer sets, {open} and {closed}. The number of answer sets is the number of possible worlds the program describes.
Often, automated reasoning paradigms in AI mimic human reasoning, providing a formalisation of the human basic inferences. Abductive reasoning is one such paradigm, and it can be seen as a formalisation of human abductive reasoning and hypotheses making:
Hypotheses make up for lack of information, and can be put forward to (deductively) support the explanation of some observations.
Abductive logic programming (ALP) [Kakas et al., 1992] is an extension of logic programming in which the knowledge base may contain special atoms that can be assumed to be true, even if they are not defined, or cannot be proven — these atoms are called abducible atoms. Starting from a goal G, an abductive derivation tries to verify G by using deductive inference steps as in LP, as well as by possibly assuming that some abducibles are true.
To help that process converge to a meaningful explanation, an abductive theory normally comes together with a set of integrity constraints (IC), which provide consistency criteria for hypotheses. The interaction is the same one Chapter 7’s BDI agents live with: hypotheses must explain the observation and stay consistent with what is known.
Model checking [Clarke et al., 1999] is an automatic technique for formally verifying finite-state concurrent systems, successfully applied in computer science to verify properties of distributed software systems. The process consists of three steps:
Model checking is the most spectacular inversion of the chapter: instead of proving a conjecture from assumptions, it builds a finite model of the system and checks the property on it by exhaustive state-space exploration — search again, but over a finite space, so the procedure always terminates.
Although model checking has been mainly used for verification of distributed systems, several proposals aim at exploiting it in the verification of intelligent systems, in particular multi-agent systems (MAS). The issues to be faced come from MAS properties besides temporal evolution (as usual in model checking): such as the mental attitudes of agents — knowledge, beliefs, desires, intentions — which require temporal logic to be combined with modal (epistemic) logics. This is the verification-side counterpart of Chapter 7’s BDI model: the same mental attitudes that drive an agent’s behaviour become the properties we check of it.
The first application area of non-classical automated reasoning is reasoning about actions — the logical side of what Chapter 10 will treat as planning.
The most famous approach is situation calculus, proposed by John McCarthy [McCarthy and Hayes, 1969]:
The deck’s example formula: p(s) → q(result(a, s)) means that, if p holds in situation s, then q will hold after executing action a. The term result(a, s) denotes the situation obtained by executing action a in situation s.
An alternative logical representation of actions is by means of modal logic [Bull and Segerberg, 1984]: there, each modality represents an action. The formula □(p → [a]q) has the same meaning as the previous example — if p holds, q will hold after execution of a — given that □φ means that φ is true (holds) in each state (situation).
Since the semantics of modal logic is based on the so-called possible worlds, it is rather natural to adopt it for reasoning about actions, by associating possible worlds with states and transitions between worlds with actions.
The deck briefly mentions the siblings: event calculus [Mueller, 2008], a logical language for representing and reasoning about events and their effects — reasoning about change; and fluent calculus [Thielscher, 1998], a formalism for expressing dynamical domains in FOL, as a variant of the situation calculus, whose main difference is that situations are considered as representations of states.
And it closes with the critical issue, the frame problem [Hanks and McDermott, 1986]: the problem of specifying in an efficient way what are the fluents that do not change from one situation to the next one when an action is executed. Every action changes a few fluents; everything else stays as it was — and writing that down naively explodes. The frame problem is the deep reason why reasoning about actions is hard, and it will reappear in Chapter 10 as the frame axiom problem of STRIPS-style planning.
Broadly speaking, logic has played a role in three aspects of software development — and in particular in the design and development of MAS [van der Hoek and Wooldridge, 2008]:
And the deck’s example ties the whole course together: BDI logics [Wooldridge, 2000] for specifying and programming agents and MAS — the very logics behind Chapter 7’s BDI architecture. The three roles map onto the chapter’s machinery: specification uses the representational power of non-classical logics (section 12); programming uses extensions of logic programming (sections 14–16); verification uses model checking (section 17).
The three roles are not alternatives; they compose. In the same MAS project, a BDI logic may specify the agents, a Jason-like language may program them, and a temporal-epistemic model checker may verify that the program satisfies the specification. Automated reasoning is the common substrate of all three.
The deck closes with the web, where automated reasoning is becoming an essential issue in many web systems and applications, especially in emerging Semantic Web applications [Hendler and van Harmelen, 2008]. The aim of the Semantic Web initiative is to advance the state of the web through the use of semantics.
Various formalisms have already emerged, like RDF or OWL, an ontology language stemming from description logics [Baader et al., 2008] — the decidable fragment of logic that section 12 introduced. So far, reasoning on the Semantic Web is mostly reasoning about knowledge expressed in a particular ontology; next steps might involve combinations of logic programming and description logics, possibly with non-monotonic extensions — e.g., answer set programming.
And finally web services (WS) have emerged as the key paradigm for the interaction and coordination of distributed business processes. The ability to automatically reason about web services — for instance to verify some properties or to compose them — could be an essential step towards the integration of agents and WS; in particular, for WS composition, orchestration, coordination. The deck notes one concrete line of work: linear logic has been exploited for automatic composition of semantic WS [Rao et al., 2004].
Closing the chapter: agents + services + semantics. Automated reasoning began as the attempt to mechanise mathematical proof; it ends here as the glue of distributed intelligent systems — exactly the setting Chapter 11 will discuss as agents and tools.
Determining whether a conjecture φ, representing a property to be verified, is a logical consequence of a set S of assumptions, which express properties of the object of study (a system, a circuit, a program, a data type, a communication protocol, a mathematical structure). The conjoint problem is knowledge representation: finding suitable formalisms for S and φ to represent aspects of the real world, such as action, space, time, mental events, and commonsense reasoning.
Classical logic has been the principal formalism in automated reasoning, with many proof techniques studied and implemented. Non-classical logics — modal, temporal, description, or nonmonotonic — have been widely investigated as means to formally represent knowledge.
Deductive theorem proving is concerned precisely with the entailment problem S |= φ. Inductive theorem proving [Hsiang and Srivas, 1987] asks whether S entails all ground instances of φ: S |= φσ for every substitution σ making φσ a ground formula.
The vast majority of theorem-proving methods work refutationally: they prove that φ follows logically from S by showing that S ∪ {¬φ} generates a contradiction, or is inconsistent. The canonical instance is SLD resolution in logic programming [Robinson, 1965], where an atom G is proven by refuting the goal ← G against the program.
Automated model building [Caferra et al., 2004] tries to answer the entailment question negatively: given assumptions S and conjecture φ, it disproves φ by finding a counter-example, or counter-model — that is, a model of S ∪ {¬φ}. If such a model exists, φ is not a logical consequence of S.
In classical FOL, deductive theorem proving is semi-decidable: if φ follows from S, a terminating proof procedure exists; otherwise the procedure may either terminate or not. Inductive theorem proving and model building are not even semi-decidable. In higher-order logics, which quantify over functions and predicates too, even deductive theorem proving is no longer semi-decidable.
Fully automated theorem proving focuses on deductive theorem proving; induction, model generation, and reasoning in higher-order logics resort to a larger extent to interactive theorem proving.
It is guaranteed to halt and return a proof if S ∪ {¬φ} is inconsistent. If it halts without a proof, we can conclude that S ∪ {¬φ} is consistent, and try to extract a model from its output. However, if S ∪ {¬φ} is consistent, the procedure is not guaranteed to halt.
Proofs of inconsistency, if they exist, are finite — yet there is an infinite search space of logical consequences in which to look for a contradiction. A machine can explore only a finite part of that infinite space, so the challenge is to find a proof using as few computational resources as possible.
An expansion rule is sound if what is generated is a logical consequence of the premises — e.g., resolution and paramodulation [Nieuwenhuis and Rubio, 2001]. A contraction rule is sound if what is removed is a logical consequence of what is left or added — e.g., subsumption [Bonacina and Hsiang, 1994] and equational simplification [Bachmair and Ganzinger, 1994]. An inference system is sound if all its rules are sound; it is refutationally complete if it allows deriving a contradiction whenever the initial set of formulae is inconsistent.
SAT is the decidable satisfiability problem of propositional logic [Franco and Martin, 2009]; many problems in computer science can be encoded in propositional logic, reduced to SAT and submitted to SAT solvers — e.g., bounded model checking [Biere et al., 2003]. DPLL (Davis–Putnam–Logemann–Loveland) [Davis et al., 1962] is the dominating approach for complete SAT solvers.
Because decidable does not mean computationally tractable: decidable reasoning problems are typically NP-complete. Overall, automated reasoning problems range from decidable (but NP-complete) to semi-decidable, or not even semi-decidable — hence the reliance on the AI paradigm of search.
A strategy is composed of an inference system and a search plan. The inference system is a non-deterministic set of inference rules that defines the search space of all possible inferences. The search plan guides the search and determines the unique derivation S0 ⊢ S1 ⊢ ... from input S0 = S ∪ {¬φ}, deciding at each step which inference rule (expansion or contraction) to apply to which data. It is the addition of the search plan that turns a non-deterministic inference system into a deterministic proof procedure.
They employ search only indirectly, or at the meta-level, since the search is made of both automated and human-driven steps. An interactive session generates a proof plan — a sequence of actions to reach a proof — where actions may be chosen by the user or by the search plan. An action can be the application of an inference rule, the introduction of a lemma by the user, or the invocation of an automated first-order prover or a decision procedure.
Hardware/software verification and program generation [Schumann, 2001] — cryptographic protocols, message-passing systems, software specifications; other fields of AI — planning, learning, natural language understanding; symbolic computation — constraint problem solving, computer algebra; computational logic — declarative programming, deductive databases; mathematics — non-trivial theorems in Boolean algebras, rings, groups, quasigroups, many-valued logic.
Two strategies: develop automated deduction techniques directly for those logics — e.g., tableau proof methods; or translate formulas of non-classical logic into formulas of classical logic, so users of non-classical logics can exploit state-of-the-art first-order theorem proving tools.
Traditional logics, even non-classical ones, are not suitable to express revisable inferences, which are the conceptual scope of nonmonotonic logics for nonmonotonic reasoning [Hanks and McDermott, 1986]. Commonsense reasoning is revisable: new information can retract conclusions. Classical logic is monotonic — adding assumptions never removes conclusions — which is precisely what commonsense reasoning needs to escape.
NAF [Clark, 1978]: to prove a negated goal ¬G, Prolog tries to prove G; if G cannot be proved, then ¬G succeeds, and vice versa. It is nonmonotonic because adding new formulas can make a previously not-provable goal G become true — and, as a consequence, ¬G might become false. The most widely accepted semantics is the answer set semantics [Gelfond, 2008], where a logic program may have several alternative models, each a possible view of the world.
ASP [Lifschitz, 2008] is an approach to negation in logic programming. Syntactically ASP programs look like Prolog programs, but the computational mechanisms are different — more like SAT solvers. An ASP computation results in 0, 1, or n sets of propositions justified by the program (its answer sets), rather than in a single computed answer at a time.
Example 1 (no negation: high_salary ← employed, educated; educated ← high_salary; employed ← motivated; motivated ←): the only justified set is {motivated, employed}, since neither high_salary nor educated can be derived. Example 2 (with negation: open ← not closed; closed ← not open): both {open} and {closed} can be justified, each by assuming the other is not derived — two possible worlds.
ALP [Kakas et al., 1992] is an extension of logic programming in which the knowledge base may contain abducible atoms — atoms that can be assumed true even if they are not defined or cannot be proven. Starting from a goal G, an abductive derivation verifies G by deductive steps as in LP plus possibly assuming some abducibles are true; integrity constraints provide consistency criteria for the hypotheses.
(1) The software system is translated into a formalism where actions are represented as states and transitions — the model. (2) The properties to be verified are specified as a formula φ, usually in temporal logic [Emerson, 1990]. (3) The verification that φ holds in the model is performed, depending on whether the temporal logic is branching-time or linear-time [Lamport, 1980].
Besides temporal evolution, MAS properties involve the mental attitudes of agents — knowledge, beliefs, desires, intentions — which require temporal logic to be combined with modal (epistemic) logics.
In the situation calculus [McCarthy and Hayes, 1969], situations are logical terms describing the state of the world; fluents are predicates varying from situation to situation. The formula means: if p holds in situation s, then q will hold after executing action a — since result(a, s) is the situation obtained by executing a in s.
The problem of specifying in an efficient way what are the fluents that do not change from one situation to the next one when an action is executed [Hanks and McDermott, 1986]. Every action changes a few fluents; specifying naively that everything else is unchanged explodes. Event calculus [Mueller, 2008] and fluent calculus [Thielscher, 1998] are alternative formalisms facing it.
As a specification language, as a programming language, and as a verification language [van der Hoek and Wooldridge, 2008]. The deck’s example: BDI logics [Wooldridge, 2000] for specifying and programming agents and MAS.
The Semantic Web advances the web through semantics: formalisms like RDF and OWL (an ontology language stemming from description logics [Baader et al., 2008]) support reasoning about knowledge expressed in ontologies, with possible combinations of LP and description logics, even with non-monotonic extensions like ASP. For web services, automatic reasoning can verify properties or compose services — e.g., linear logic has been exploited for automatic composition of semantic WS [Rao et al., 2004].