Synthesis of positive logic programs for checking a class of definitions with infinite quantification (Q2629858)

The framework is based on typed first-order logic theories such as the following: Types: {\parindent=0.7cm\begin{itemize}\item[--] Nat generated by \(\mathrm{zero}:\rightarrow\mathrm{Nat}\quad\mathrm{succ}:\mathrm{Nat}\rightarrow\mathrm{Nat}\) \item[--] Seq generated by \(\mathrm{empty}:\rightarrow\mathrm{Seq}\quad\mathrm{succ}:\mathrm{Nat}\times\mathrm{Seq}\rightarrow\mathrm{Seq}\) \end{itemize}} Predicates: \(\mathrm{id}:\mathrm{Nat}\times\mathrm{Nat}\) axiomatised as: {\parindent=0.7cm\begin{itemize}\item[--] \(\mathrm{id}(\mathrm{zero},\mathrm{zero})\Leftrightarrow \mathrm{true}\) \item[--] \(\forall(\mathrm{id}(\mathrm{succ}(X),\mathrm{zero})\Leftrightarrow\mathrm{false})\) \item[--] \(\forall(\mathrm{id}(\mathrm{zero},\mathrm{succ}(Y)\Leftrightarrow\mathrm{false})\) \item[--] \(\forall(\mathrm{id}(\mathrm{succ}(X),\mathrm{succ}(Y))\Leftrightarrow\mathrm{id}(X,Y))\) \end{itemize}} \(\mathrm{member}:\mathrm{Nat}\times\mathrm{Seq}\) axiomatised as: {\parindent=0.7cm\begin{itemize}\item[--] \(\forall(\mathrm{member}(E,\mathrm{empty})\Leftrightarrow\mathrm{false})\) \item[--] \(\forall(\mathrm{member}(E,\mathrm{seq}(X,Y ))\Leftrightarrow\mathrm{id}(E,X)\vee\mathrm{member}(E,Y ))\) \end{itemize}} The authors consider \textit{assertion definitions} of the form \(\forall X(r(X)\Leftrightarrow Q Y R(X,Y))\) where \(r\) is the defined relation, \(Q\) is a quantifier, and \(R\) is the defining relation, namely, a quantifier-free formula in the language of the typed first-order logic theory. For example, the following is an assertion definition for the subset relation: \[ \forall L,S(\mathrm{subset}(L,S)\Leftrightarrow\forall E(\mathrm{member}(E,L)\Rightarrow\mathrm{member}(E,S))) \] The purpose of the paper is a method to synthesise a positive logic program for checking assertions of the form \(r(X)\theta\), where \(\theta\) is a ground substitution for \(X\), that depends on the quantifier \(Q\) in such a way that if \(Q\) is \(\forall\) then the program searches for refutations, whereas if \(Q\) is \(\exists\) then the program searches for proofs. The method satisfies both key requirements: {\parindent=0.7cm\begin{itemize}\item[--] the synthesis process terminates after a finite amount of transformation steps; \item[--] the synthesised program preserves total correctness w.r.t. the class of goals of the form \(\Leftarrow r(X,Y)\theta\). \end{itemize}} With the example of the subset relation, the synthesised program is: \[ \begin{aligned} \forall(\mathrm{subset}(L,S) \Leftarrow \mathrm{subset}_1(E,L,S))\\ \forall(\mathrm{subset}_1(E,\mathrm{seq}(X,Y ),S) \Leftarrow \mathrm{subset}_2(E,S)\wedge \mathrm{subset}_3(E,X))\\ \forall(\mathrm{subset}_1(E,\mathrm{seq}(X,Y ),S)\Leftarrow \mathrm{subset}_1(E,Y ,S)\wedge \mathrm{subset}_4(E,X))\\ \forall(\mathrm{subset}_1(E,\mathrm{empty},S) \Leftarrow \mathrm{subset}_5(E,S))\\ \forall(\mathrm{subset}_2(E,\mathrm{seq}(X,Y )) \Leftarrow \mathrm{subset}_2(E,Y )\wedge \mathrm{subset}_4(E,X))\\ \forall(\mathrm{subset}_2(E,\mathrm{empty}) \Leftarrow \mathrm{subset}_7)\\ \mathrm{subset}_3(\mathrm{zero},\mathrm{zero}) \Leftarrow \mathrm{subset}_9\\ \forall(\mathrm{subset}_3(\mathrm{succ}(X),\mathrm{succ}(Y )) \Leftarrow \mathrm{subset}_3(X,Y ))\\ \forall(\mathrm{subset}_4(\mathrm{zero},\mathrm{succ}(Y )) \Leftarrow \mathrm{subset}_9)\\ \forall(\mathrm{subset}_4(\mathrm{succ}(X),\mathrm{succ}(Y )) \Leftarrow \mathrm{subset}_4(X,Y ))\\ \forall(\mathrm{subset}_4(\mathrm{succ}(X),\mathrm{zero}) \Leftarrow \mathrm{subset}_9)\\ \forall(\mathrm{subset}_5(E,\mathrm{seq}(X,Y )) \Leftarrow \mathrm{subset}_5(E,Y )\wedge \mathrm{subset}_4(E,X))\\ \mathrm{subset}_7 \Leftarrow\\ \mathrm{subset}_9 \Leftarrow\end{aligned} \] following a procedure that consists of 6 steps, with intermediate formulas generated on the way, in particular: \[ \begin{aligned}\forall E,L,S(\mathrm{subset}_1(E,L,S)\Leftrightarrow(\mathrm{member}(E,L)\wedge\neg\mathrm{member}(E,S)))\\ \forall(\mathrm{subset}_2(X,Y )\Leftrightarrow\mathrm{true}\wedge\neg\mathrm{member}(X,Y ))\\ \forall(\mathrm{subset}_3(X,Y )\Leftrightarrow\mathrm{id}(X,Y ))\\ \forall(\mathrm{subset}_4(X,Y )\Leftrightarrow\neg\mathrm{id}(X,Y ))\\ \forall(\mathrm{subset}_5(X,Y )\Leftrightarrow\mathrm{false}\wedge\neg\mathrm{member}(X,Y ))\\ \mathrm{subset}_6\Leftrightarrow\mathrm{false}\wedge\neg\mathrm{false}\\ \mathrm{subset}_7\Leftrightarrow\mathrm{true}\wedge\neg\mathrm{false}\\ \mathrm{subset}_8\Leftrightarrow\mathrm{true}\wedge\neg\mathrm{true}\\ \mathrm{subset}_9\Leftrightarrow\mathrm{true}\\ \mathrm{subset}_{10}\Leftrightarrow\neg\mathrm{true}\end{aligned} \] The method has been tested with many other assertion definitions, listed in the appendix, together with the proofs of termination and correctness.