Skip to main content
Engineering LibreTexts

3.E: First Order Logic and Automated Reasoning in a Nutshell (Excercises)

  • Page ID
    6410
  • \( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)

    \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)

    \( \newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\)

    ( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\)

    \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)

    \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\)

    \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)

    \( \newcommand{\Span}{\mathrm{span}}\)

    \( \newcommand{\id}{\mathrm{id}}\)

    \( \newcommand{\Span}{\mathrm{span}}\)

    \( \newcommand{\kernel}{\mathrm{null}\,}\)

    \( \newcommand{\range}{\mathrm{range}\,}\)

    \( \newcommand{\RealPart}{\mathrm{Re}}\)

    \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)

    \( \newcommand{\Argument}{\mathrm{Arg}}\)

    \( \newcommand{\norm}[1]{\| #1 \|}\)

    \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)

    \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\AA}{\unicode[.8,0]{x212B}}\)

    \( \newcommand{\vectorA}[1]{\vec{#1}}      % arrow\)

    \( \newcommand{\vectorAt}[1]{\vec{\text{#1}}}      % arrow\)

    \( \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)

    \( \newcommand{\vectorC}[1]{\textbf{#1}} \)

    \( \newcommand{\vectorD}[1]{\overrightarrow{#1}} \)

    \( \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} \)

    \( \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} \)

    \( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)

    \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)

    \(\newcommand{\avec}{\mathbf a}\) \(\newcommand{\bvec}{\mathbf b}\) \(\newcommand{\cvec}{\mathbf c}\) \(\newcommand{\dvec}{\mathbf d}\) \(\newcommand{\dtil}{\widetilde{\mathbf d}}\) \(\newcommand{\evec}{\mathbf e}\) \(\newcommand{\fvec}{\mathbf f}\) \(\newcommand{\nvec}{\mathbf n}\) \(\newcommand{\pvec}{\mathbf p}\) \(\newcommand{\qvec}{\mathbf q}\) \(\newcommand{\svec}{\mathbf s}\) \(\newcommand{\tvec}{\mathbf t}\) \(\newcommand{\uvec}{\mathbf u}\) \(\newcommand{\vvec}{\mathbf v}\) \(\newcommand{\wvec}{\mathbf w}\) \(\newcommand{\xvec}{\mathbf x}\) \(\newcommand{\yvec}{\mathbf y}\) \(\newcommand{\zvec}{\mathbf z}\) \(\newcommand{\rvec}{\mathbf r}\) \(\newcommand{\mvec}{\mathbf m}\) \(\newcommand{\zerovec}{\mathbf 0}\) \(\newcommand{\onevec}{\mathbf 1}\) \(\newcommand{\real}{\mathbb R}\) \(\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}\) \(\newcommand{\laspan}[1]{\text{Span}\{#1\}}\) \(\newcommand{\bcal}{\cal B}\) \(\newcommand{\ccal}{\cal C}\) \(\newcommand{\scal}{\cal S}\) \(\newcommand{\wcal}{\cal W}\) \(\newcommand{\ecal}{\cal E}\) \(\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}\) \(\newcommand{\gray}[1]{\color{gray}{#1}}\) \(\newcommand{\lgray}[1]{\color{lightgray}{#1}}\) \(\newcommand{\rank}{\operatorname{rank}}\) \(\newcommand{\row}{\text{Row}}\) \(\newcommand{\col}{\text{Col}}\) \(\renewcommand{\row}{\text{Row}}\) \(\newcommand{\nul}{\text{Nul}}\) \(\newcommand{\var}{\text{Var}}\) \(\newcommand{\corr}{\text{corr}}\) \(\newcommand{\len}[1]{\left|#1\right|}\) \(\newcommand{\bbar}{\overline{\bvec}}\) \(\newcommand{\bhat}{\widehat{\bvec}}\) \(\newcommand{\bperp}{\bvec^\perp}\) \(\newcommand{\xhat}{\widehat{\xvec}}\) \(\newcommand{\vhat}{\widehat{\vvec}}\) \(\newcommand{\uhat}{\widehat{\uvec}}\) \(\newcommand{\what}{\widehat{\wvec}}\) \(\newcommand{\Sighat}{\widehat{\Sigma}}\) \(\newcommand{\lt}{<}\) \(\newcommand{\gt}{>}\) \(\newcommand{\amp}{&}\) \(\definecolor{fillinmathshade}{gray}{0.9}\)

    Exercise \(\PageIndex{1}\)

    What is the difference between syntax and semantics for a logic?

    Exercise \(\PageIndex{2}\)

    What is a theory?

    Exercise \(\PageIndex{3}\)

    Name the four core components for automated reasoning.

    Exercise \(\PageIndex{4}\)

    Describe the procedure for tableau reasoning in four shorts sentences.

    Exercise \(\PageIndex{1}\)

    Write in one natural language sentence what the following sentences in First-Order Logic state.

    a. \(\forall x(Lion(x)\to Mammal(x))\)

    b. \(\forall x(PC(x)\to\exists y,z(hasPart(x,y)\wedge connected(x,z)\wedge CPU(y)\wedge Monitor(z)))\)

    c. \(\forall x,y(hasProperPart(x,y)\to\neg hasProperPart(y,x))\)

    Answer

    (a) All lions are mammals.

    (b) Each PC has as part at least one CPU and at least one Monitor connected

    (c) Proper part is asymmetric.

    Exercise \(\PageIndex{2}\)

    Formalize the following natural language sentence into First-Order Logic.

    a. Each car is a vehicle.

    b. Every human parent has at least one human child.

    c. Any person cannot be both a lecturer and a student editor of the same course.

    Answer

    (a) \(\forall x(Car(x)\to Vehicle(x))\)

    (b) \(\forall x(HumanParent(x)\to\exists y(haschild(x,y)\wedge Human(y)))\)

    (c) \(\forall x,y(Person(x)\wedge Course(y)\to\neg (lecturerOf(x,y)\wedge studentOf(x,y)))\)

    Exercise \(\PageIndex{3}\)

    Consider the structures in Figure 2.3.2, which are graphs.

    a. Figures 2.3.2-A and B are different depictions, but have the same descriptions w.r.t. the vertices and edges. Check this.

    Screenshot (59).png

    Figure 2.3.1: Explanation of the tableaux in Figure 2.2.2.

    b. C has a property that A and B do not have. Represent this in a first-order sentence.

    c. Find a suitable first-order language for A (/B), and formulate at least two properties of the graph using quantifiers.

    Screenshot (60).png

    Figure 2.3.2: Graphs for Exercise 2.3.3 (figures A-C) and Exercise 2.3.4 (figure D).

    Answer

    (b) There exists a node that does not participate in an instance of \(R\), or: it does not relate to anything else: \(\exists x\forall y.\neg R(x,y)\).

    (c) \(\mathcal{L} =\langle R \rangle\) as the binary relation between the vertices. Optionally, on can add the vertices as well. Properties:

    \(R\) is symmetric: \(\forall xy.R(x,y)\to R(y,x)\).

    \(R\) is irreflexive: \(\forall x.\neg R(x,x)\).

    If you take into account the vertices explicitly, one could say that each note participates in at least two instances of \(R\) to different nodes.

    Exercise \(\PageIndex{4}\)

    Consider the graph in Figure 2.3.2, and first-order language \(\mathcal{L} =\langle R\rangle\), with \(R\) being a binary relation symbol (edge).

    a. Formalize the following properties of the graph as \(\mathcal{L}\)-sentences:

    (i) \((a, a)\) and \((b, b)\) are edges of the graph;

    (ii) \((a, b)\) is an edge of the graph;

    (iii) \((b, a)\) is not an edge of the graph. Let \(T\) stand for the resulting set of sentences.

    b. Prove that \(T\cup\{\forall x\forall yR(x,y)\}\) is unsatisfiable using tableaux calculus.

    Answer

    (a) \(R\) is reflexive (a thing relates to itself): \(\forall x.R(x,x)\) ∀x.R(x, x).

    \(R\) is asymmetric (if \(a\) relates to \(b\) through relation \(R\), then \(b\) does not relate back to \(a\) through \(R\)): \(\forall xy.R(x,y)\to\neg R(y,x)\).

    Exercise \(\PageIndex{5}\)

    Let us have a logical theory \(\Theta\) with the following sentences:

    • \(\forall xPizza(x), \forall xPizzaT(x), \forall xPizzaB(x)\), which are disjoint
    • \(\forall x(Pizza(x) \to\neg PizzaT(x))\),
    • \(\forall x(Pizza(x)\to\neg PizzaB(x))\),
    • \(\forall x(PizzaT(x)\to\neg PizzaB(x))\),
    • \(\forall x,y(hasT(x,y)\to Pizza(x)\wedge PizzaT(y))\),
    • \(\forall x,y(hasB(x,y)\to Pizza(x)\wedge PizzaB(y))\),
    • \(\forall x(ITPizza(x)\to Pizza(x))\), and
    • \(\forall x(ITPizza(x)\to\neg\exists y(hasT(x,y)\wedge FruitT(y))\), where
    • \(\forall x(VegeT(x)\to PizzaT(x))\) and
    • \(\forall x(Fruit(x)\to PizzaT(x))\).

    Task (read in full first before attempting it):

    a. A Pizza margherita has the necessary and sufficient conditions that it has mozzarella, tomato, basilicum and oil as toppings and has a pizza base. Add this to \(\Theta\). Annotate you commitments: what have you added to \(\Theta\) and how? Hint: fruits are not vegetables, categorize the toppings, and “necessary and sufficient” is denoted with \(\leftrightarrow\).

    b. We want to merge our new \(\Theta\) with some other theory \(\Gamma\) that has knowledge about fruits and vegetables. \(\Gamma\) contains, among other formulas, \(\forall x(Tomato(x)\to Fruit(x))\). What happens? Represent the scenario formally, and prove your answer.

    Actually, this is not easy to figure out manually, and there are ways to automate this, which you will do later in Chapter 4.


    This page titled 3.E: First Order Logic and Automated Reasoning in a Nutshell (Excercises) is shared under a CC BY 4.0 license and was authored, remixed, and/or curated by Maria Keet via source content that was edited to the style and standards of the LibreTexts platform.