Commit b6edecde authored by Łukasz Czajka's avatar Łukasz Czajka
Browse files

paper: related work

parent 6f505f5a
@book{Wallen1990,
Author = {L.A. Wallen},
Publisher = {{MIT} Press},
Title = {Automated proof search in non-classical logics},
Year = {1990}}
Author = {L.A. Wallen},
Publisher = {{MIT} Press},
Title = {Automated proof search in non-classical logics},
Year = {1990}}
@incollection{Waaler2001,
author = {A. Waaler},
booktitle = {Handbook of Automated Reasoning},
editor = {J. A. Robinson and A. Voronkov},
volume = {2},
pages = {1487--1578},
publisher = {Elsevier and {MIT} Press},
title = {Connections in Nonclassical Logics},
year = {2001}}
@article{MillerNadathurPfenningScedrov1991,
Author = {D. Miller and G. Nadathur and F. Pfenning and A. Scedrov},
Journal = {Ann. Pure Appl. Log.},
Number = {1-2},
Pages = {125--157},
Title = {Uniform Proofs as a Foundation for Logic Programming},
Volume = {51},
Year = {1991}}
Author = {D. Miller and G. Nadathur and F. Pfenning and A. Scedrov},
Journal = {Ann. Pure Appl. Log.},
Number = {1-2},
Pages = {125--157},
Title = {Uniform Proofs as a Foundation for Logic Programming},
Volume = {51},
Year = {1991}}
@book{Dragalin1988,
author = {A. G. Dragalin},
publisher = {American Mathematical Society},
series = {Translations of mathematical monographs},
title = {Mathematical Intuitionism: Introduction to Proof Theory},
volume = {76},
year = {1988}}
@article{Simmons2014,
Author = {R.J. Simmons},
Journal = {{ACM} Trans. Comput. Log.},
Number = {3},
Pages = {21:1--21:33},
Title = {Structural Focalization},
Volume = {15},
Year = {2014}}
Author = {R.J. Simmons},
Journal = {{ACM} Trans. Comput. Log.},
Number = {3},
Pages = {21:1--21:33},
Title = {Structural Focalization},
Volume = {15},
Year = {2014}}
@article{LiangMiller2009,
Author = {C. Liang and D. Miller},
Journal = {Theor. Comput. Sci.},
Number = {46},
Pages = {4747--4768},
Title = {Focusing and polarization in linear, intuitionistic, and classical logics},
Volume = {410},
Year = {2009}}
Author = {C. Liang and D. Miller},
Journal = {Theor. Comput. Sci.},
Number = {46},
Pages = {4747--4768},
Title = {Focusing and polarization in linear, intuitionistic, and classical logics},
Volume = {410},
Year = {2009}}
@inproceedings{Otten2016a,
Author = {J. Otten},
Booktitle = {ARQNL 2016},
Pages = {9--20},
Title = {Non-clausal Connection-based Theorem Proving in Intuitionistic First-Order Logic},
Year = {2016}}
@inproceedings{Otten1995,
author = {J. Otten},
booktitle = {{TABLEAUX} '95},
pages = {122--137},
title = {A Connection Based Proof Method for Intuitionistic Logic},
year = {1995}}
@book{Bibel1987a,
Author = {W. Bibel},
Publisher = {Vieweg},
Title = {Automated theorem proving, 2nd Edition},
Year = {1987}}
Author = {W. Bibel},
Publisher = {Vieweg},
Title = {Automated theorem proving, 2nd Edition},
Year = {1987}}
@inproceedings{ReedLovelandSmith1991,
author = {D. W. Reed and D. W. Loveland and B. T. Smith},
booktitle = {ELP'91},
pages = {345--369},
publisher = {Springer},
series = {{LNCS}},
title = {The Near-{H}orn Approach to Disjunctive Logic Programming},
volume = {596},
year = {1991}}
@inproceedings{NadathurLoveland1995,
author = {G. Nadathur and D. W. Loveland},
booktitle = {{LICS} '95},
pages = {148--155},
publisher = {{IEEE} Computer Society},
title = {Uniform Proofs and Disjunctive Logic Programming},
year = {1995}}
@incollection{NadathurLoveland1998,
author = {G. Nadathur and D. W. Loveland},
booktitle = {Handbook of Logic in Artificial Intelligence and Logic Programming},
editor = {D. M. Gabbay and C. J. Hogger and J. A. Robinson},
publisher = {Clarendon Press},
title = {Proof procedures for logic programming},
volume = {5},
year = {1998}}
@book{LoboMinkerRajasekar1992,
author = {J. Lobo and J. Minker and A. Rajasekar},
publisher = {{MIT} Press},
series = {Logic Programming},
title = {Foundations of disjunctive logic programming},
year = {1992}}
@book{TroelstraSchwichtenberg1996,
Author = {A.S. Troelstra and H. Schwichtenberg},
Publisher = {Cambridge University Press},
Title = {Basic Proof Theory},
Year = {1996}}
Author = {A.S. Troelstra and H. Schwichtenberg},
Publisher = {Cambridge University Press},
Title = {Basic Proof Theory},
Year = {1996}}
@article{IRIS2018,
Author = {R. Jung and R. Krebbers and J.{-}H. Jourdan and A. Bizjak and L. Birkedal and D. Dreyer},
Journal = {J. Funct. Program.},
Pages = {e20},
Title = {Iris from the ground up: {A} modular foundation for higher-order concurrent separation logic},
Volume = {28},
Year = {2018}}
@inproceedings{MulderKrebbers2021,
Author = {Ike Mulder and Robbert Krebbers},
Booktitle = {TYPES 2021},
Title = {Towards automation for {Iris}},
Year = {2021}}
Author = {R. Jung and R. Krebbers and J.{-}H. Jourdan and A. Bizjak and L. Birkedal and D. Dreyer},
Journal = {J. Funct. Program.},
Pages = {e20},
Title = {Iris from the ground up: {A} modular foundation for higher-order concurrent separation logic},
Volume = {28},
Year = {2018}}
@unpublished{MulderKrebbersGeuvers2021,
Author = {Ike Mulder and Robbert Krebbers and Herman Geuvers},
Note = {Submitted},
Title = {Diaframe: Automated Verification of Fine-Grained Concurrent Programs in {Iris}},
Year = {2021}}
@inproceedings{MulderKrebbersGeuvers2022,
author = {Ike Mulder and Robbert Krebbers and Herman Geuvers},
booktitle = {PLDI '22},
title = {Diaframe: Automated Verification of Fine-Grained Concurrent Programs in {Iris}},
year = {2022}}
......@@ -112,15 +112,15 @@ for disjunction.
Disjunction is difficult to incorporate into intuitionistic
backward-chaining proof search in a goal-directed manner, because in
the corresponding sequent calculus applications of the right rules for
disjunction cannot always be permuted below applications of the left
rules. It is therefore unclear when to eliminate disjunctions on the
left. For instance, to show $\alpha \lor \beta \proves \beta \lor
\alpha$ first the disjunction on the left needs to be eliminated, and
only afterwards a disjunct on the right can be chosen. In the above
example, the disjunction on the left could be eagerly eliminated, but
this is in general not possible when the disjunction is the target of
a hypothesis of the form e.g.~$\forall \vec{x} . \varphi_1 \to \ldots
the corresponding sequent calculus the right rules for disjunction
cannot always be permuted below the left rules. It is therefore
unclear when to eliminate disjunctions on the left. For instance, to
show $\alpha \lor \beta \proves \beta \lor \alpha$ first the
disjunction on the left needs to be eliminated, and only afterwards a
disjunct on the right can be chosen. In the above example, the
disjunction on the left could be eagerly eliminated, but this is in
general not possible when the disjunction is the target of a
hypothesis of the form e.g.~$\forall \vec{x} . \varphi_1 \to \ldots
\to \varphi_n \to \alpha \lor \beta$. In the language with only
conjunction, implication and universal quantification, or more
generally for hereditary Harrop
......@@ -149,24 +149,96 @@ intuitionistic sequent calculus, a simple variant of which we present
in Section~\ref{sec_prop} for intuitionistic propositional logic. The
general approach may be adapted to various non-classical logics. We
implement and evaluate the practicality of our approach in the
Diaframe automation tool for the Iris~\cite{IRIS2018} framework of
higher-order concurrent intuitionistic separation logic. Our
adaptation of the approach to the logic of Iris does not yield a
complete proof search procedure, but the evaluation suggests that it
significantly improves Diaframe's automation and is strong enough for
many practical examples involving disjunction.
Preliminary investigations indicate that, at the cost of substantial
complications, our approach to handling disjunction in
backward-chaining proof search could be developed into a complete
calculus for first-order intuitionistic logic and probably other
non-classical logics. The structures such a calculus would need to
manipulate, however, would be substantially more complex than
multi-succedent sequents. We leave the detailed development of such a
complete calculus for future work.
Diaframe~\cite{MulderKrebbersGeuvers2022} automation tool for the
Iris~\cite{IRIS2018} framework of higher-order concurrent
intuitionistic separation logic. Our adaptation of the approach to the
logic of Iris does not yield a complete proof search procedure, but
the evaluation suggests that it significantly improves Diaframe's
automation and is strong enough for many practical examples involving
disjunction.
The main advantage of our approach is that it can be relatively easily
incorporated into backward-chaining proof search procedures used in
hand-crafted automation in proof assistants. The point is to
significantly improve automation for disjunction on practically
occurring examples which typically include many features outside of
first-order logic. For this purpose, theoretical completeness is not
essential and simplicity is preferable.
\subsection{Related work}
[TODO: talk about Diaframe and Iris]
Our idea for goal-directed handling of disjunction in
backward-chaining proof search, while simple in its basic formulation,
relates to and draws inspiration from diverse previous work in proof
theory.
One way to see our approach is as an adaptation of uniform
proofs~\cite{MillerNadathurPfenningScedrov1991} to handle disjunctions
in the targets of hypotheses. Disjunctive logic
programming~\cite{LoboMinkerRajasekar1992} and near-Horn
Prolog~\cite{ReedLovelandSmith1991,NadathurLoveland1995,NadathurLoveland1998}
are based on similar ideas.
The basic calculus we present in Section~\ref{sec_prop} is a focused
version of a fragment of Dragalin's intuitionistic multi-succedent
calculus~\cite{Dragalin1988}. Focusing~\cite{Simmons2014,LiangMiller2009}
addresses the issue of rule non-permutability by dividing proof search
into two alternating phases: the inversion phase in which invertible
rules are eagerly applied, and the focusing phase which groups
sequences of non-invertible rules. This limits backtracking to the
choice of focus in the focusing phase, significantly reducing the
search space.
Focusing by itself does not directly address the issue of the
irrelevance of rule applications. Irrelevance means that a rule does
not contribute to the derivation of the sequent. For instance, to
derive the sequent $\varphi_1 \lor \varphi_2, \alpha \land \beta
\proves \alpha$ it is possible but not necessary to first apply the
left rule for disjunction to decompose $\varphi_1\lor\varphi_2$. The
sequent may more easily be derived by just applying the left
conjunction rule to~$\alpha \land \beta$ and then the
axiom. Decomposing a disjunction unnecessarily may incur significant
overhead since it generates two subgoals. In the inversion phase of
focused proof search, the invertible rules are applied eagerly
regardless of whether they are necessary to complete a
derivation. Ordinarly, left focusing (i.e.~focusing on a formula on
the left side of a sequent) stops at a disjunction and switches to the
inversion phase in which the disjunction is then split. But there is
no explicit mechanism to limit the choice of focus to formulas whose
decomposition contributes to the final derivation.
Connection calculi~\cite{Waaler2001,Wallen1990,Otten1995} address both
the issues of non-permutability and irrelevance with connection-guided
proof search. For propositional logic, a connection is a pair of a
positive and a negative occurrence of the same atom. To take into
account non-permutability of rules, a notion of a complementary
connection is introduced which depends on the logic. In terms of the
sequent calculus, a complementary connection corresponds to the
principal formulas in an initial sequent at the leaf of a
derivation. Connection calculi identify a connection first, then in
essence directly reduce the sequent to obtain the corresponding
initial sequent~\cite[\textsection3]{Wallen1990}.
Our approach analogously relies on identifying a ``connection''
between a positive atom occurrence on the right and a (unifiable) atom
occurring in the target of a hypothesis. An incomplete variant of this
approach may be formulated as a focused multi-succeedent sequent
calculus where left focusing does not stop at disjunctions (see the
next section). Leaving detailed investigations for future work, we
only briefly remark on our belief that the analogy with connection
calculi goes beyond purely superficial. One way of making the calculus
from the next section complete could be by labelling the formulas with
inuitionisitc prefixes like in the free variable
calculi~\cite[Section~4]{Waaler2001} directly related to connection
calculi. The resulting calculus would be a focused version of a
labelled free variable calculus essentially incorporating a fixed
backward-chaining connection-driven search strategy into the
formalism. From the perspective of the Curry-Howard isomorphism, the
prefixes essentially describe pointers into the structure of
incomplete proof terms.
\section{Disjunction in propositional intuitionistic
logic}\label{sec_prop}
......@@ -183,9 +255,10 @@ focus. By $\Gamma,\varphi$ we denote the multiset
$\Gamma \cup \{\varphi\}$.
Our calculus is a focused version of a fragment of Dragalin's
intuitionistic multi-succedent sequent calculus. As usual in focused
calculi, proof search is divided into two phases: the inversion phase
and the focusing phase. In the inversion phase, the rules are applied
intuitionistic multi-succedent sequent
calculus~\cite{Dragalin1988}. As usual in focused calculi, proof
search is divided into two phases: the inversion phase and the
focusing phase. In the inversion phase, the rules are applied
eagerly. Backtracking is limited to the focusing phase and the choice
of focus. To avoid pointless choices, in an implementation one could
e.g.~store with each formula the set of its atomic targets.
......@@ -258,9 +331,10 @@ $\Gamma;[\alpha'\to\alpha]\proves[\alpha];\alpha,\beta$, which
requires deriving $\Gamma\proves\alpha'$. The only possibility is then
to try to derive $\Gamma;[\alpha'\lor\beta']\proves[\alpha'];\alpha'$,
which generates the subgoal $\Gamma,\beta'\proves\alpha'$. Trying to
prove this subgoal will always generate the same subgoal. Analogously,
focusing on~$\beta$ on the right does not allow us to construct a
derivation either.
prove this subgoal will always generate the same subgoal with
additional occurrences of~$\beta'$ on the left. Analogously, focusing
on~$\beta$ on the right does not allow us to construct a derivation
either.
One remedy is to extend the calculus with a judgement form
$\Gamma\proves[\varphi];\Delta$, change the rule $L{\to}$ to
......@@ -284,29 +358,25 @@ and add the following right-focusing rules:
\]
In terms of the Curry-Howard isomorphism, one could see the above
calculus as constructing proof terms bottom-up, inserting case
expressions (eliminators for disjunction) only immediately after
variables introduced by lambdas or case expressions, i.e., lifting
case expressions out of applications. We believe that one could extend
the above ideas to a goal-directed calculus complete for first-order
intuitionistic logic which would directly manipulate sequences of
lambda terms with holes, progressively refining the holes, inserting
case expressions and eliminators for existentials as early in the term
as possible. In this setting, universal quantification is analogous to
implication and existential quantification to disjunction (both are
inductive types). A sequent calculus formulation obscures this
analogy.
calculus as constructing proof terms in two phases: a top-down phase
which creates abstractions, pairs and injections, and a bottom-up
phase which creates applications, projections and case expressions
(eliminators for disjunction), inserting the case expressions only
immediately after variables introduced by lambdas or case expressions,
i.e., lifting them out of applications. Preliminary investigations
indicate that one could extend the above ideas to a goal-directed
calculus complete for first-order intuitionistic logic which would
directly manipulate sequences of lambda terms with holes
(corresponding to a stack of current subgoals), progressively refining
the holes, inserting case expressions and eliminators for existentials
as early in the proof term sequence as possible. In this setting,
universal quantification is analogous to implication and existential
quantification to disjunction (both are inductive types). A sequent
calculus formulation obscures this analogy.
In this paper, we do not attempt to devise a complete calculus for
intuitionistic logic along the above lines. Instead, we evaluate the
practicality of the general approach by an implementation in
Diaframe. The main advantage of our approach is that it can be
relatively easily incorporated into backward-chaining proof search
procedures used in hand-crafted automation in proof assistants. The
point is to significantly improve automation for disjunction on
practically occurring examples which typically include many features
outside of first-order logic. For this purpose, theoretical
completeness is not essential and simplicity is preferable.
practicality of the general approach by an implementation in Diaframe.
\section{Extending Diaframe to handle disjunction}
......
Supports Markdown
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