Packages

final case class Sequent(ante: IndexedSeq[Formula], succ: IndexedSeq[Formula]) extends Product with Serializable

Sequent ante |- succ with antecedent ante and succedent succ.

ante(0),ante(1),...,ante(n) |- succ(0),succ(1),...,succ(m)

This sequent is often pretty-printed with signed line numbers:

    -1: ante(0)
    -2: ante(1)
        ...
-(n+1): ante(n)
 ==> 1: succ(0)
     2: succ(1)
        ...
 (m+1): succ(m)

The semantics of sequent ante |- succ is the conjunction of the formulas in ante implying the disjunction of the formulas in succ.

ante

The ordered list of antecedents of this sequent whose conjunction is assumed.

succ

The orderd list of succedents of this sequent whose disjunction needs to be shown.

See also

Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143-189, 2008.

Linear Supertypes
Serializable, Serializable, Product, Equals, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Sequent
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. AnyRef
  7. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Sequent(ante: IndexedSeq[Formula], succ: IndexedSeq[Formula])

    ante

    The ordered list of antecedents of this sequent whose conjunction is assumed.

    succ

    The orderd list of succedents of this sequent whose disjunction needs to be shown.

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. val ante: IndexedSeq[Formula]
  5. def apply(pos: SuccPos): Formula

    Retrieves the formula in sequent at a given antecedent position.

    Retrieves the formula in sequent at a given antecedent position.

    pos

    the antecedent position of the formula

    returns

    the formula at the given position from the antecedent

    Note

    slightly faster version with the same result as Sequent.apply(SeqPos)

  6. def apply(pos: AntePos): Formula

    Retrieves the formula in sequent at a given succedent position.

    Retrieves the formula in sequent at a given succedent position.

    pos

    the succedent position of the formula

    returns

    the formula at the given position from the succedent

    Note

    slightly faster version with the same result as Sequent.apply(SeqPos)

  7. def apply(pos: SeqPos): Formula

    Retrieves the formula in sequent at a given position.

    Retrieves the formula in sequent at a given position.

    pos

    the position of the formula

    returns

    the formula at the given position either from the antecedent or the succedent

  8. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  9. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  10. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  11. def finalize(): scala.Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  12. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. def glue(s: Sequent): Sequent

    A copy of this sequent concatenated with given sequent s.

    A copy of this sequent concatenated with given sequent s. Sequent(A,S) glue Sequent(B,T) == Sequent(A++B, S++T)

    s

    the sequent whose antecedent to append to ours and whose succedent to append to ours.

    returns

    a copy of this sequent concatenated with s. Results in a least upper bound with respect to subsets of this and s.

  14. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  15. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. final def notify(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  17. final def notifyAll(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  18. def prettyString: String

    Pretty-print sequent

  19. def sameSequentAs(r: Sequent): Boolean

    Check whether this sequent is the same as the given sequent r (considered as sets)

    Check whether this sequent is the same as the given sequent r (considered as sets)

    Note

    Used for contracts in the core.

  20. def subsequentOf(r: Sequent): Boolean

    Check whether this sequent is a subsequent of the given sequent r (considered as sets)

    Check whether this sequent is a subsequent of the given sequent r (considered as sets)

    Note

    Used for contracts in the core.

  21. val succ: IndexedSeq[Formula]
  22. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  23. def toString(): String
    Definition Classes
    Sequent → AnyRef → Any
  24. def updated(p: SuccPos, s: Sequent): Sequent
  25. def updated(p: AntePos, s: Sequent): Sequent
  26. def updated(p: SeqPos, s: Sequent): Sequent

    A copy of this sequent with the indicated position replaced by gluing the sequent s.

    A copy of this sequent with the indicated position replaced by gluing the sequent s.

    p

    the position of the replacement

    s

    the sequent glued / concatenated to this sequent after dropping p.

    returns

    a copy of this sequent with the formula at position p removed and the sequent s appended.

    See also

    Sequent.glue(Sequent)

    Sequent.updated(Position,Formula)

  27. def updated(p: SuccPos, f: Formula): Sequent
  28. def updated(p: AntePos, f: Formula): Sequent
  29. def updated(p: SeqPos, f: Formula): Sequent

    A copy of this sequent with the indicated position replaced by the formula f.

    A copy of this sequent with the indicated position replaced by the formula f.

    p

    the position of the replacement

    f

    the replacing formula

    returns

    a copy of this sequent with the formula at position p replaced by f.

  30. final def wait(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  31. final def wait(arg0: Long, arg1: Int): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  32. final def wait(arg0: Long): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from AnyRef

Inherited from Any

Ungrouped