diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-06-15 10:30:07 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-15 10:30:07 -0700 |
| commit | 786574dff56615972fe89fca81c4f7a517ef16d9 (patch) | |
| tree | 1877fe37fab101be202e2d0739d88b3ee2bb1e95 /docs/theories/separation-logic.rst | |
| parent | ac0146e4142587df45dada4bdf9e0d0faec81a67 (diff) | |
docs: Add references instead of links in theory reference pages. (#6729)
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: |