Docs / Semantics / Aspect / Instantiation

Instantiation of sorted properties

import Linglib.Semantics.Aspect.Instantiation · namespace Aspect

Source

This file defines the instantiation of a sorted property at a reference interval. An event property is instantiated when the run time of one of its events lies in the interval, a state property when the run time of one of its states overlaps it, as in the discourse representation analyses of Kamp and Rohrer, Partee, and Kamp and Reyle, and a property of times when it holds of the interval. Reference intervals are Interval (WithTop T), so an interval may run to the end of time and the null interval is ⊥.

Main definitions

Main results

References

Declarations

A sorted property is a property of events, of states, or of times.

inductive SortedPropertyL46–50
(W : Type u_4) (E : Type u_5) (T : Type u_6) [LinearOrder T] :
Type (max (max u_4 u_5) u_6)

Used by SortedProperty.IsEventuality, At, exists_mem_of_at, not_at_bot, At.mono

Used in Cariani2021, Condoravdi2002

At t w Q says that the property Q is instantiated in w at the interval t, by inclusion of the runtime for events, overlap for states, and application for properties of times.

def AtL59–64
{W : Type u_1} {E : Type u_2} {T : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (t : Interval (WithTop T)) (w : W) :
SortedProperty W E T → Prop

Built from

Used by exists_mem_of_at, not_at_bot, At.mono, at_Ici_eventive_iff, at_Ici_stative_iff, at_eventive_withTop_iff_prfv, at_stative_withTop_of_unbounded

Used in Cariani2021, Condoravdi2002