Raisonnement automatisée : Principes et applications

Raisonnement Automatis´e: Principes etApplications (partie I: logique du premier ordre)N. Peltier (CNRS, Universit´e de Grenoble)2009This document contains the first part of the M2R course RAPA: AutomatedReasoning: Principle and Applications. It presents the basis of first-order logicand automated deduction: syntax, semantics, transformation into clausal form,unification and the Resolution calculus (with selection functions and atom or-dering). Some basic properties of the Resolution calculus are also investigated(w.r.t. complexity and termination).This document is self-contained but additional references are provided forthe interested reader. More details and additional explanations can be found in[5,6]. [8]isanadvancedtextboookontheResolutioncalculusandtheHandbookof Automated Reasoning [12] covers the main lines of research in this field.1 First Order LogicFirst-order logic (FOL) is a formal language for expressing properties. Propo-sitional logic allows one to express basic statements (s.t. “Paris is a town” or“Berlinis atown”or“Parisisthe capitalofFrance”)andto combinethem withlogical connectives:¬ (not),∨ (or),∧ (and),⇒ (implies) and⇔ (equivalence).First-orderlogic extends this languageby using predicate symbols and quantifi-cation over individuals. For instance, the property “to be a town” may be ex-pressedby a predicatesymbol Town, which can be applied to differentindividu-als: Town(Paris),Town(Berlin),...Usingquantification ...