From 2189d01c6498c9926c39b7b2883aab32f6b059ea Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Sun, 3 Jan 2016 18:41:06 +0100 Subject: [PATCH] solution for 3a --- a2/3.tex | 27 ++++++++++++++++++++++++--- a2/pre.tex | 1 + a2/src/3a.prvr9 | 8 ++++---- 3 files changed, 29 insertions(+), 7 deletions(-) diff --git a/a2/3.tex b/a2/3.tex index c2c610f..a7b1b60 100644 --- a/a2/3.tex +++ b/a2/3.tex @@ -68,10 +68,31 @@ tools rather than elaborating the questions by hand.} \textsc{prover9} fails to find a proof for $x*y=y*x$. Running the same file with \textsc{mace4} gives the following - counterexample. - - + counterexample listed in Table~\ref{tab:s3a}. + \begin{table}[H] + \centering + \begin{tabular}{llll} + $G=\{0,1,2,3,4,5\}$ & $I=0$ & + $inv(x)=\left\{\begin{array}{ll} + x=3 & 4\\ + x=4 & 3\\ + \text{else} & x + \end{array}\right.$ & + $x*y=\left\{\begin{array}{ll|llllll} + & & \multicolumn{6}{c}{x}\\ + & & 0& 1 & 2 & 3 & 4 & 5\\ + \hline + \multirow{6}{*}{y}& 1 & 0 & 1 & 2 & 3 & 4 & 5\\ + & 1 & 1 & 0 & 3 & 2 & 5 & 4\\ + & 2 & 2 & 4 & 0 & 5 & 1 & 3\\ + & 3 & 3 & 5 & 1 & 4 & 0 & 2\\ + & 4 & 4 & 2 & 5 & 0 & 3 & 1\\ + & 5 & 5 & 3 & 4 & 1 & 2 & 0 + \end{array}\right.$ + \end{tabular} + \caption{Solution for problem 3a}\label{tab:s3a} + \end{table} \item\emph{A term rewrite system consists of the single rule $$a(x,a(y,a(z,u)))\rightarrow a(y,a(z,a(x,u))),$$ in which $a$ is a binary symbol and $x,y,z,u$ are variables. diff --git a/a2/pre.tex b/a2/pre.tex index 5fc61c6..cd9af74 100644 --- a/a2/pre.tex +++ b/a2/pre.tex @@ -9,6 +9,7 @@ \usepackage{float} % For nice tables \usepackage{graphicx} \usepackage{xypic} +\usepackage{multirow} \everymath{\displaystyle} diff --git a/a2/src/3a.prvr9 b/a2/src/3a.prvr9 index 812fdd4..a12d73d 100644 --- a/a2/src/3a.prvr9 +++ b/a2/src/3a.prvr9 @@ -1,11 +1,11 @@ formulas(assumptions). all x all y all z (x*(y*z)=(x*y)*z). -all x (x*I=x). -all x (x*inv(x)=I). +all x (x*a=x). +all x (x*inv(x)=a). end_of_list. formulas(goals). -%I*x=x. +%a*x=x. %inv(inv(x))=x. -%inv(x)*x=I. +%inv(x)*x=a. all x all y (x*y=y*x). end_of_list. -- 2.20.1