Skip to content
Snippets Groups Projects
Commit b47721d9 authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Proof simple subproofs, metaterms, remove tabs

parent 28d75df5
No related branches found
No related tags found
No related merge requests found
Pipeline #7259 failed
Stage: test
    Hide whitespace changes
    Inline Side-by-side
    Showing
    with 102 additions and 78 deletions
    spec/doc.tex
    + 102
    − 78
    View file @ b47721d9
    ......@@ -485,8 +485,8 @@ understand the proof intuitively.
    A proof in the Alethe language is an indexed list of steps.
    To mimic the concrete syntax we write a step in the form
    \begin{plListEq}
    c_1,\,\dots,\, c_k &\proofsep i. & \varphi_1,\dots ,\varphi_l &
    (\ruleType{rule}\; p_1,\,\dots,\, p_n)\,[a_1,\,\dots,\,a_m]
    c_1,\,\dots,\, c_k &\proofsep i. & \varphi_1,\dots ,\varphi_l &
    (\ruleType{rule}\; p_1,\,\dots,\, p_n)\,[a_1,\,\dots,\,a_m]
    \end{plListEq}
    \noindent
    Each step has a unique index \(i \in \mathbb{I}\), where \(\mathbb{I}\) is a countable
    ......@@ -548,8 +548,8 @@ A \proofRule{subproof} step can not use premise from a subproof nested within th
    \begin{comment}{Mathias Fleury}
    There are two ways to export one element from the subproof:
    \begin{itemize}
    \item rely on the order and take the last one
    \item add an explicit :premises in the conclusion stop to give the exported step
    \item rely on the order and take the last one
    \item add an explicit :premises in the conclusion stop to give the exported step
    \end{itemize}
    \end{comment}
    ......@@ -640,17 +640,17 @@ In the following a concluding rule is a proof rule that concludes a
    subproof (such as \proofRule{subproof} and \proofRule{bind}).
    \begin{definition}[Calculated Context]
    Let $s_i$ be a step or anchor in $P$ such that no step $s_j$
    where $j < i$ uses a concluding
    rule. Let $a_1, \dots, a_m$ be the anchors among $s_1, \dots, s_{i-1}$.
    Let $s_i$ be a step or anchor in $P$ such that no step $s_j$
    where $j < i$ uses a concluding
    rule. Let $a_1, \dots, a_m$ be the anchors among $s_1, \dots, s_{i-1}$.
    The calculated context of $s_i$ is the context
    $c_{1,1}, \dots, c_{1, n_1}, \dots, c_{m,1}, \dots, c_{m, n_m}$
    where $c_{k,1}, \dots, c_{k, n_k}$ is the context of $a_k$.
    The calculated context of $s_i$ is the context
    $c_{1,1}, \dots, c_{1, n_1}, \dots, c_{m,1}, \dots, c_{m, n_m}$
    where $c_{k,1}, \dots, c_{k, n_k}$ is the context of $a_k$.
    Note that if $s_i$ is an anchor, its calculated context is the
    context before concatenating it with the context associated
    with $s_i$.
    Note that if $s_i$ is an anchor, its calculated context is the
    context before concatenating it with the context associated
    with $s_i$.
    \end{definition}
    To check the validity of a proof we can inductively eliminate subproofs
    ......@@ -671,30 +671,28 @@ Of course this is only valid if the steps that are replace do not contain
    partial subpoors. Due to our induction, we will only replace entire subproofs that
    do not contain subpoof.
    \begin{definition}[Admissible Proof, Pure Subproofs]
    Let $P_i$ be the proof $[s_1, \dots, s_n]$ and $1 \leq \mathit{start}
    < \mathit{end} \leq n$ such that
    \begin{itemize}
    \item $s_{\mathit{start}}$ is an anchor,
    \item $s_{\mathit{end}}$ is a step that uses a concluding rule,
    \item no $s_k$ with $\mathit{start} < k < \mathit{end}$ is an anchor or
    a step that uses a concluding rule.
    \end{itemize}
    The proof $P_i$ is \emph{admissible} if it either contains no such $\mathit{start}$,
    $\mathit{end}$, or
    \begin{itemize}
    \item all steps $s_k$ with $\mathit{start} < k <
    \mathit{end}$ only use the premises $s_l$ with $\mathit{start} <
    l < k$,
    \item all steps $s_k$ are valid application of their rule under the
    calculated context of $s_{\mathit{start}}$,
    \item the step $s_{\mathit{end}}$ is a valid application of its rule
    under its calculated context,
    \item the proof $P_{i+1}$, where the steps $s_{\mathit{start}}, \dots,
    s_{\mathit{end}}$ have been replaced by $s'$ as described above, is admissible.
    \end{itemize}
    We call the admissible proof $[s_{\mathit{start}}, \dots, s_{\mathit{end}}]$ a \emph{pure
    subproof}.
    \begin{definition}[Admissible Proof]
    Let $P_i$ be the proof $[s_1, \dots, s_n]$ and $1 \leq \mathit{start}
    < \mathit{end} \leq n$ such that
    \begin{itemize}
    \item $s_{\mathit{start}}$ is an anchor,
    \item $s_{\mathit{end}}$ is a step that uses a concluding rule,
    \item no $s_k$ with $\mathit{start} < k < \mathit{end}$ is an anchor or
    a step that uses a concluding rule.
    \end{itemize}
    The proof $P_i$ is \emph{admissible} if it either contains no such $\mathit{start}$,
    $\mathit{end}$, or
    \begin{itemize}
    \item all steps $s_k$ with $\mathit{start} < k <
    \mathit{end}$ only use the premises $s_l$ with $\mathit{start} <
    l < k$,
    \item all steps $s_k$ are valid application of their rule under the
    calculated context of $s_{\mathit{start}}$,
    \item the step $s_{\mathit{end}}$ is a valid application of its rule
    under its calculated context,
    \item the proof $P_{i+1}$, where the steps $s_{\mathit{start}}, \dots,
    s_{\mathit{end}}$ have been replaced by $s'$ as described above, is admissible.
    \end{itemize}
    \end{definition}
    Since proofs are finite, this process stops at some admissible proof
    ......@@ -704,19 +702,19 @@ $P_{\mathit{last}}$. Otherwise, we can check $P_{\mathit{last}}$ to
    see if the overall proof is valid.
    \begin{definition}[Valid Alethe Proof]
    An Alethe proof $P_0 = [s_1, \dots, s_n]$ is valid if
    \begin{itemize}
    \item $P_0$ does not contain any step that uses the \proofRule{hole} rule,
    \item each step in $P_0$ uses an unique index,
    \item $P_0$ is admissible,
    \item $P_0$ contains a step that has the empty clause as its conclusion,
    \item $P_{\mathit{last}}$ does not contain any anchor or step using a concluding
    rule,
    \item all steps $s_k$ in $P_{\mathit{last}}$
    only use the premises $s_l$ with $1 \leq l < k$,
    \item all steps in $P_{\mathit{last}}$ are valid
    applications of their rules under the empty context.
    \end{itemize}
    An Alethe proof $P_0 = [s_1, \dots, s_n]$ is valid if
    \begin{itemize}
    \item $P_0$ does not contain any step that uses the \proofRule{hole} rule,
    \item each step in $P_0$ uses an unique index,
    \item $P_0$ is admissible,
    \item $P_0$ contains a step that has the empty clause as its conclusion,
    \item $P_{\mathit{last}}$ does not contain any anchor or step using a concluding
    rule,
    \item all steps $s_k$ in $P_{\mathit{last}}$
    only use the premises $s_l$ with $1 \leq l < k$,
    \item all steps in $P_{\mathit{last}}$ are valid
    applications of their rules under the empty context.
    \end{itemize}
    \end{definition}
    In this document we will often call $P_{\mathit{last}}$ the outermost
    ......@@ -725,7 +723,8 @@ proof.
    \subsubsection{Soundness}
    To show the soundness of a valid Alethe proof $P = [s_1, \dots, s_n]$
    we can use the same induction as the for the definition of validity.
    we can use the same approach as for the definition of validity: consider
    subproof free subproofs and then replace subproofs by holes.
    \begin{theorem}[Soundness of Alethe]
    If there is a valid Alethe proof $P$ that has the formulas
    ......@@ -736,28 +735,53 @@ steps in its outermost proof, then
    \]
    \end{theorem}
    We wills start with simple subproofs with empty contexts and then add contexts.
    We wills start with simple subproofs without subproofs and with empty contexts.
    Here, we will assume that every rule is sound.
    \begin{lemma}
    Let $P = [s_1, \dots, s_n]$ be a pure subpoof such that no $s_i$ is
    an anchor, $s_n$ is a \proofRule{subproof} step with the conclusion
    $\psi$, and $\varphi_1, \dots, \varphi_m$ are the conclusion of \proofRule{assume}
    steps. Then $\vDash \varphi_1, \dots, \varphi_m \limp \psi$.
    Let $P = [s_{\mathit{start}}, \dots, s_{\mathit{end}}]$ be an
    admissible proof such that no $s_i$ with $ i> 1$ is an anchor,
    $s_{\mathit{end}$ is a \proofRule{subproof} step with the
    conclusion $\psi$, and $\varphi_1, \dots, \varphi_m$ are the
    conclusion of \proofRule{assume} steps. Then $\vDash \varphi_1,
    \dots, \varphi_m \limp \psi$.
    \end{lemma}
    \begin{proof}
    Let $s_j$ be the premise of the step $s_n$. Due to the definition of
    \proofRule{subproof}, this conclusion of $s_j$ is $\psi$. If we can
    show that $s_j$ means $\varphi_1, \dots, \varphi_m \vDash \psi$,
    then $\vDash \varphi_1, \dots, \varphi_m \limp \psi$ since
    \proofRule{subproof} is sound.
    We show this by induction over the proof steps. Let $V_0 = \emptyset$.
    Let $\psi_i$ be the conclusions of the step $s_i$. If $s_i$ is an
    \proofRule{assume} step, then let $V_i = V_{i-1} \cup \{\psi_i\}$.
    Otherwies,
    By induction over the proof steps we can show that for each step $s_i$ with
    the conclusion $\psi_i$ it holds that $V_i \vDash \psi_i$ where
    $V_i$ is the set formulas assumed before $s_i$.
    Let $V_0 = \emptyset$.
    Let $\psi_i$ be the conclusions of the step $s_i$. If $s_i$ is an
    \proofRule{assume} step, then let $V_i = V_{i-1} \cup \{\psi_i\}$.
    Otherwise, let $S$ be the set of premises of $s_i$ and $P$ the set
    of the conclusions of the steps in $S$.
    Since $s_i$ is a valid application of its rule, we have $P \vDash \psi_i$.
    Now, for every step $s_j \in S$ with the conclusion $\psi_j \in P$, we
    have $j < i$ and $V_j \vDash \psi_j$ due to the induction hypothesis. Since $j < i$, the
    premises $V_j$ are a subset of $V_i$ and we can weaken $V_j \vDash \psi_j$ to
    $V_i \vDash \psi_j$. Consequently, $V_i \vDash \psi_i$.
    This process ends when $s_{\mathit{end}}$ is reached and we
    get $\varphi_1, \dots, \varphi_n \vDash \psi$ and by definition of
    \proofRule{subproof} $\vDash \varphi_1, \dots, \varphi_m \limp \psi$.
    \end{proof}
    To clarify the subproofs with contexts, we translate the contexts into
    $\lambda$-terms. For a deeper description of this approach see the
    publication that introduced this approach~\cite{barbosa-2019}.
    These $\lambda$-terms are called \emph{metaterms}
    \begin{definition}[Metaterm]
    Metaterms are expressions constructed by the grammar
    \[
    M \,::=\, \boxed{t}\,\mid\, \lambda x.\,M\,\mid\,(\lambda \bar{x}_n.\,
    M)\,\bar{t}_n
    \]
    \end{definition}
    \subsubsection{Abstract Inference System} % or Rules, or Rules of Inference
    \label{sec:inference-system}
    Most of the content is taken from the presentation and the correctness proof of
    ......@@ -1250,22 +1274,22 @@ remove the steps of the subproof from memory after checking it.
    There is an open question with regard to the best way to print
    subproofs:
    There is an implicit relation between the last step of the subproof
    There is an implicit relation between the last step of the subproof
    and the step concluding the subproof.
    {\textrightarrow} what if we would, for some reason, have some crap after the last step
    of the subproof? We cannot accommodate this yet.
    There are multiple solutions to solve this implicit dependency.
    There are multiple solutions to solve this implicit dependency.
    {\textbullet} One is to
    give the final step of the subproof as a premise to the step concluding
    the subproof.
    {\textrightarrow} downside: normally it's forbidden to use steps from within a deeper proof
    {\textbullet} One is to
    give the final step of the subproof as a premise to the step concluding
    the subproof.
    {\textrightarrow} downside: normally it's forbidden to use steps from within a deeper proof
    {\textbullet} We could have the conclusion of the subproof already in the anchor.
    or we could turn the current structure upside down
    {\textrightarrow} downside: a solver that just dumps out steps can not no always know
    the conclusion when opening a subproof. For example, when simplifications are applied.
    {\textbullet} We could have the conclusion of the subproof already in the anchor.
    or we could turn the current structure upside down
    {\textrightarrow} downside: a solver that just dumps out steps can not no always know
    the conclusion when opening a subproof. For example, when simplifications are applied.
    \end{comment}
    \subsection*{Sharing and Skolem Terms}
    ......@@ -1492,7 +1516,7 @@ f(t_1, \dots, t_n) \simeq f(u_1, \dots, u_n)\) \\
    P(t_1, \dots, t_n) \simeq P(u_1, \dots, u_n)\) \\
    \ruleref{qnt_cnf} & Clausification of a quantified formula. \\
    \ruleref{and_pos} & \(\neg (\varphi_1 \land \dots \land \varphi_n) , \varphi_k \) \\
    \ruleref{and_neg} & \( (\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1 , \dots , \neg\varphi_n \) \\
    \ruleref{and_neg} & \( (\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1 , \dots , \neg\varphi_n \) \\
    \ruleref{or_pos} & \( \neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots , \varphi_n \) \\
    \ruleref{or_neg} & \( (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k \) \\
    \ruleref{xor_pos1} & \( \neg (\varphi_1 \operatorname{xor} \varphi_2) , \varphi_1 , \varphi_2 \) \\
    ......@@ -1610,7 +1634,7 @@ Rule & Description \\
    \ruleref{and_pos} & \(\neg (\varphi_1 \land \dots \land \varphi_n), \varphi_k\)\\
    \ruleref{and_neg} & \((\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1, \dots , \neg\varphi_n \) \\
    \ruleref{or_pos} & \(\neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots
    , \varphi_n \) \\
    , \varphi_n \) \\
    \ruleref{or_neg} &
    \( (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k \)\\
    \ruleref{xor_pos1} &
    ......
    0% or .
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment