diff options
Diffstat (limited to 'docs/theories/separation-logic.rst')
-rw-r--r-- | docs/theories/separation-logic.rst | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst index c2dcda78e..43c114404 100644 --- a/docs/theories/separation-logic.rst +++ b/docs/theories/separation-logic.rst @@ -7,10 +7,9 @@ language. Signature --------- -Given a (decidable) base theory :math:`T`, cvc5 has a -`decision procedure <https://cvc4.github.io/publications/2016/RIS+16.pdf>`__ -for quantifier-free :math:`SL(T)_{Loc,Data}` formulas, where :math:`Loc` and -:math:`Data` are any sort belonging to :math:`T`. +Given a (decidable) base theory :math:`T`, cvc5 implements a decision procedure +for quantifier-free :math:`SL(T)_{Loc,Data}` formulas :cite:`ReynoldsIS016`, +where :math:`Loc` and :math:`Data` are any sort belonging to :math:`T`. A :math:`SL(T)_{Loc,Data}` formula is one from the following grammar: |