jagomart
digital resources
picture1_Calculus All Formula Pdf 172260 | Lics17


 136x       Filetype PDF       File size 0.40 MB       Source: www.irif.fr


File: Calculus All Formula Pdf 172260 | Lics17
constructive completeness for the linear time calculus amina doumane irif universite paris diderot cnrs doumane irif fr abstract modal calculus is one of the central logics for really met since ...

icon picture PDF Filetype PDF | Posted on 27 Jan 2023 | 2 years ago
Partial capture of text on file.
                                              Constructive completeness
                                          for the linear-time µ-calculus
                                                                     Amina Doumane
                                                                         ´
                                                        IRIF, Universite Paris Diderot & CNRS
                                                                      doumane@irif.fr
                Abstract—Modal µ-calculus is one of the central logics for       really met, since the only existing algorithm is the naive one,
             verification. In his seminal paper, Kozen proposed an axiomati-      that enumerates all µLK proofs.
             zation for this logic, which was proved to be complete, 13 years      Aproof of completeness is a mathematical argument show-
             later, by Kaivola for the linear-time case and by Walukiewicz       ing that every valid formula is provable, but it is not always
             for the branching-time one. These proofs are based on complex,      possible to extract from such argument an algorithm that pro-
             non-constructive arguments, yielding no reasonable algorithm
             to construct proofs for valid formulas. The problematic of          duces proofs for valid formulas. Indeed, completeness proofs
             constructiveness becomes central when we consider proofs as         may involve complex, non-constructive arguments yielding no
             certificates, supporting the answers of verification tools. In our    method for actually constructing a proof. On the contrary, a
             paper, we provide a new completeness argument for the linear-       constructive proof of completeness, specifying a proof search
             time µ-calculus which is constructive, i.e. it builds a proof       method, readily provides a “realistic” algorithm.
             for every valid formula. To achieve this, we decompose this
             difficult problem into several easier ones, taking advantage of        None of the existing proofs of completeness for the µ-
             the correspondence between the µ-calculus and automata theory.      calculus w.r.t. Kozen’s axiomatization ([4], [5]) is constructive
             More precisely, we lift the well-known automata transformations     in this sense. All the attempts to get constructive proofs were
             (non-determinization for instance) to the logical level. To solve   either partial (Kozen provided a constructive completeness
             each of these smaller problems, we perform first a proof-search in   proof for the fragment of aconjunctive formulas [6]); or fall out
             a circular proof system, then we transform the obtained circular
             proofs into proofs of Kozen’s axiomatization.                       of Kozen’s axiomatization. Indeed, in his first completeness
                                   I. INTRODUCTION                               result [7], Walukiewicz had to modify Kozen’s axiomatization
                                                                                 to get a constructive proof for an ad-hoc proof system.
                The linear-time µ-calculus [1] is a temporal logic that ex-        In this paper, we provide a constructive proof for the full
             tends Pnueli’s Linear Temporal Logic (LTL) [2] with least and       linear-time µ-calculus w.r.t. µLK. To do so, we go back to the
             greatest fixed points. This increases considerably its expressive    earlier proofs of completeness, and try to understand where
             power while keeping the decidability properties of LTL, which       constructiveness is lost, to better solve this problem.
             makes it a very suitable logic for verification. The linear-time       Earlier proofs of completeness for the µ-calculus rely
             µ-calculus has infinite words as models, thus it can be used         schematically on the following idea. Find a subset C2 of the
             to express trace properties of reactive systems. There exist,       set of µ-calculus formulas C1 such that:
             among others, two approaches to verification using temporal            1) For every valid formula ϕ in C , there is a valid formula
             logics [3]. The first one, called “model theoretic”, describes                                       1     1
                                                                                       ϕ in C such that ϕ ⊢ ϕ is provable.
             both the system S and the property P to check as formulas                  2      2             2     1
             ϕ and ϕ ; then verifying whether S satisfies P is reduced              2) Every valid formula of C2 is provable. This is the
               S        P                                                              completeness result restricted to C .
             to checking the validity of the formula ϕ     →ϕ . The other                                                  2
                                                         S      P                Completeness is proved by combining 1) and 2) via a cut rule:
             approach, called “proof theoretic” reduces the verification
             problem to the provability of the formula ϕ        → ϕ . The
                                                              S       P
             advantage of the second approach is that it gives, besides
             the boolean answer to the verification problem, a certificate                   2)       1)
             that supports the decision of the verification tool, which is                ⊢ϕ      ϕ ⊢ϕ                        C2       C1
                                                                                             2     2    1
             the proof of the formula ϕ     →ϕ . To make this approach                                    (Cut)
                                          S       P                                            ⊢ϕ1
             work with the linear-time µ-calculus, two conditions should
             be satisfied: the first is the existence of a sound and complete
             deductive system for the linear-time µ-calculus; the second
             is the existence of algorithms that produce proofs for valid        Thecomplexity of problems 1) and 2) depends on the class C2:
             formulas. The first condition is satisfied, since the linear-time     the larger it is, the more difficult problem 2) becomes, since
             µ-calculus enjoys a deductive system, that we call µLK, which       it gets close to the original completeness problem. On the
             is the restriction of Kozen’s axiomatization for the modal µ-       contrary, when C gets smaller, the problem 1) becomes diffi-
                                                                                                  2
             calculus to the linear time. This system was proved to be sound     cult. Kaivola’s proofs uses the class of banan form formulas;
             and complete by Kaivola ([4]). But the second condition is not      and Walukiewicz’ one uses the class of disjunctive formulas
                        negations. These classes are very small and problem 2) is easy                                                                where the three difficulties are eliminated. The proof will be
                        to prove, but problem 1) is much more involved, and this is                                                                   carried out in the following 5 steps:
                        where constructiveness is lost in both proofs.                                                                                      I                            ∀ϕ∈C ,∃A∈APWsuch that:
                             Instead of splitting the difficulty in two by introducing one                                                                                                              0
                                                                                                                                                                                        L(A)=M(ϕ) and [A]⊢                                         ϕ.
                        intermediate class, we introduce several classes C                                                 ⊆··· ⊆ C                                                                                                       µLK
                                                                                                                       n                      1             II                       ∀A∈APW,∃P∈NPWsuchthat:
                        and generalize the proof scheme used earlier:                                                                                                                  L(P)=L(A) and [P] ⊢                                      [A].
                             1) For all i ∈ [1,n[ and for every valid formula ϕ ∈                                                                                                                                                       µLK
                                                                                                                                         i                  III                      ∀P ∈NPW,∃B∈NBWsuch that:
                                    C , there is a valid formula ϕ                                          ∈ C               such that
                                      i                                                            i+1               i+1                                                                L(B) = L(P) and [B] ⊢                                   [P].
                                    ϕ         ⊢           ϕ .                                                                                                                                                                          µLK
                                       i+1       µLK         i                                                                                                                                                           ω
                             2) Every valid formula of C                                 is provable.                                                       IV         ∀B ∈ NBW, if L(B) = Σ then ∃D ∈ DBW s.t.:
                                                                                     n                                                                                                                        ω
                                                                                                                                                                                          L(D)=Σ and [D]⊢µLK [B].
                        As before, we combine these results to get completeness. The                                                                                                                                             ω
                        interest of this approach is to split the difficult problem of                                                                       V                ∀D∈DBW,if L(D)=Σ then ⊢µLK [D].
                        completeness into several easier problems, for which we can                                                                   Step IV is a bit special because in general NBW cannot be
                        hope to construct effectively a proof.                                                                                        determinized into DBW. But if a NBW B recognizes the
                                                                                                                                                      universal language Σω, there is obviously a DBW D with the
                                                                                                                                                                                                                      ¨
                                                                                                                                                      same language: the complete Buchi automaton with exactly
                                                                                                                                                      one (accepting) state for instance. This is enough for our
                                                                                                                                                      needs, since we start in the proof of completeness from a
                                                                                                                                                                                                                      ω
                           ⊢ϕ           ϕ ⊢ϕ                    . . .   ϕ ⊢ϕ                                                                          valid formula ϕ (i.e., M(ϕ) = Σ ), hence the automata A,P
                                 n         n         n−1                   2         1 (Cut)                             C ... C           C                                                                                                                              ω
                                                     ⊢ϕ                                                                    n           2     1        and B constructed in steps I-III all recognize the language Σ .
                                                           1                                                                                          To show that [D] ⊢                            [B] in step IV, we use a more general
                                                                                                                                                                                            µLK
                                                                                                                                                                                                                                                   ¨
                                                                                                                                                      result from [8], which shows that for every Buchi automata
                                                                                                                                                      B ,B such that L(B ) ⊆ L(B ) one has [B ] ⊢                                                            [B ].
                                                                                                                                                         1      2                               2                 1                          2       µLK         1
                                                                                                                                                           We now give an idea of how to prove the sequents of the
                        Now the question is how to find these classes. For that,                                                                       other steps. Actually, what makes the proof search difficult in
                        we identified three sources of complexity that make a valid                                                                    µLK, is the rule (ν) shown below, where S should be guessed.
                        formula hard to prove: i) The alternation of disjunctions and                                                                                                   Γ⊢∆,S                  S ⊢ F[S/X]
                        conjunctions, ii) The interleaving of least and greatest fixed                                                                                                                                                    (ν)
                        points, iii) The presence of disjunctions. In automata theory,                                                                                                             Γ⊢∆,νX.F
                        these sources of complexity also exist with different names:                                                                  To circumvent this problem, we go through an intermediate
                        i) Alternation (of universal and existential non-determinism),                                                                proof system where the rule (ν) just unfolds the ν-formula:
                        ii) The use of parity conditions, and iii) Non-determinism.                                                                                                          Γ⊢∆,F[νX.F/X]
                        In automata over infinite words, all these difficulties can be                                                                                                                                                (ν)
                        reduced through effective algorithms, transforming automata                                                                                                                Γ⊢∆,νX.F
                        with one of these difficulties into others without. For example,                                                               Two examples of such proof systems are the one introduced
                        one has algorithms to eliminate alternation, to reduce the                                                                    in [9] which we call µLKω                                     ,   and the one introduced in
                                                                                                                                                                                     ω                       DHL                 ω                      ω
                        number of priorities for a parity condition or to get rid of                                                                  [8], called µLK . The proofs of µLK                                             and µLKDHL, which
                        non-determinism. The correspondence between linear-time µ-                                                                    have the shape of graphs, are called circular proofs. The idea
                        calculus formulas and alternating parity word automata (APW)                                                                  is to find a circular proof for the sequent to prove, then to
                        over infinite words is now very well established. This is                                                                      transform this circular proof into a µLK one. The advantage
                        fortunate since our idea was to import these techniques from                                                                  of µLKω                 is that it is competely invertible and the proof
                                                                                                                                                                     DHL
                        the automata side to the logical one. Concretely, it is known                                                                 search is a trivial task. However, the algorithms known to
                                                                                                                                                                                                         ω
                        that we can encode every APW A by a formula [A] such                                                                          transform effectively µLK                                   proofs into µLK ones are very
                                                                                                                                                                                                         DHL
                        that the language of A equals the set of models of [A]. The                                                                   restrictive. In contrast, we have given a strong translation result
                                                                                                                                                                      ω
                        intermediate classes we will use are the following: The largest                                                               for µLK              ([8]), based on a general geometric condition on
                                                                                                                                                                                                                                                           ω
                        class, denoted [APW], is the image of APW by this encoding;                                                                   proofs. Building on this, we shall work with µLK . To get
                        this class embodies all the difficulties indicated above. The                                                                  this stronger translatability criterion, µLKω uses sequents of
                        next class is [NPW], the image of non-deterministic parity                                                                    a particular shape. Indeed, sequents are not sets of formulas,
                        automata (NPW) by this encoding. The formulas of this class                                                                   as it is the case for µLKω                               ; but are rather sets of formula
                                                                                                                                                                                                        DHL
                        do not contain the first level of complexity which is the                                                                      occurrences. The difficulty of using such sequents is that the
                        alternation ∨,∧. The third class is [NBW], the encoding of                                                                    proof system is not invertible and proving the sequents of steps
                                                                ¨                                                   ¨                                 I-V in µLKω is not immediate.
                        non-deterministic Buchi automata (NBW). Buchi automata
                        are particular cases of parity automata where only the two                                                                         Let us finally emphasize that the implications appearing in
                        priorities 0 and 1 are allowed. We can say then that in this                                                                  steps I-V are well known at the semantical level, but lifting
                        class we simplified the two difficulties i) and ii). The smallest                                                               them to the provability level is not immediate and strongly de-
                                                                                                                    ¨
                        class is [DBW], the image of deterministic Buchi automata,                                                                    pends on the encoding [ ] and the shape of automata obtained
             by the different automata transformations. To illustrate this     corresponds to an instant of time, and a letter at some position
             by an extremal example, any valid formula ϕ is semantically       represents the set of atoms true at the corresponding instant
             equivalent to ⊤ and to itself, but proving ⊤ ⊢ ϕ is as difficult   of time. In the example below, atoms p,q are true at instant
             as proving ⊢ ϕ, while proving ϕ ⊢ ϕ is immediate. In general,     0, atoms q,r are true at instant 1, etc.
             given a formula ψ semantically equivalent to ϕ, closer ψ is
             to ϕ, the easier ψ ⊢ ϕ will be to prove. That is why we will                      p,q       q,r        p        . . .
             provide for our development an encoding of automata that
             follows closely their structure; and automata transformations     We define the semantics of a formula w.r.t. a model to be the
             that do not change brutally the input automaton (or the input     set of instants of time where the formula holds in this model.
             formula for step I). That is also why we cannot treat these                                            u
                                                                               Definition 2. The semantics kϕk          of a formula F w.r.t.
             transformations as black boxes and will recall them in detail.                                         ρ
                                                                                      ω                              ω
               Organization of the paper In Section II we introduce the        u ∈ Σ and a valuation ρ : V 7→ 2         is a subset of natural
                                                                               numbers inductively defined as follows:
             linear-time µ-calculus and its semantics together with µLK             u                                   u
                                                                                kpk ={i∈ω|p∈u}                     k¬pk ={i∈ω|p∈/ u }
             andµLKω.Thenwestateasufficientconditionthatensuresthe                   ρ                  i                ρ                  i
                                                                                     u                           u                         u
                                   ω                                            kXk =ρ(X)                 k⊙ϕk ={i∈ω|i+1∈kϕk }
             translatability of µLK   proofs into µLK ones. In Section III,          ρ   u        u       u      ρ          u       u      ρu
                                                                                kϕ∨ψk =kϕk ∪kψk                    kϕ∧ψk =kϕk ∩kψk
             we present the model of APW and their encoding [ ] in the                   ρ   S ρ          ρ                 ρ       ρ        ρ
                                                                                         u                           u
                                                                                kνX.ϕk = {W ⊆ω|W ⊆kϕk                         }
             linear-time µ-calculus. Conversely, we give a way to build for              ρ   T                       ρ[X←W]
                                                                                         u                     u
                                                                                kµX.ϕk = {W ⊆ω|kϕk                      ⊆W}
             every µ-calculus formula ϕ an APW A that recognizes the set                 ρ                     ρ[X←W]
                                                    ϕ                          Suppose that ϕ is a closed formula. We write kϕku instead of
             of its models. The main result of this section is [A ] ⊢     ϕ.
                                                                 ϕ   µLK           u
                                                                               kϕk , since the semantics of ϕ do not depend on ρ. We say
             In Section IV, we recall the automata transformations that turn       ρ
                                                                                                                                    u
             an APW A into an NPW P, and P into an NBW B, all                  that ϕ is true in u, and we write u |= ϕ, if 0 ∈ kϕk . The set
             having the same language. The main results of this section        of models of ϕ is defined by M(ϕ) = {u ∈ Σω | u |= ϕ}. A
                                                                                                                                            ω
             are [B] ⊢µLK [P] and [P] ⊢µLK [A]. In Section V, we show          formula is valid if it is true in every model, ie. M(ϕ) = Σ .
             that for every NBW B recognizing the language Σω, there
             is a DBW D recrognizing also Σω, such that [D] ⊢            [B]   B. Proof systems for linear-time µ-calculus
                                                                    µLK
             and ⊢µLK [D]. We finally bring these pieces together to get a         There are many possible presentations of sequent calculus,
             constructive proof of completeness.                               which differ by the way sequents are defined. Sometimes
              II. LINEAR-TIME µ-CALCULUS AND ITS PROOF SYSTEMS                 sequents are presented as sets or multisets of formulas, but
               In this section we introduce the linear-time µ-calculus and     most proof-theoretical observations, in particular the proofs-
             its semantics, together with two proof systems. The first is       as-programs correspondence, hold in a setting where sequents
             µLK, the target of our completeness result. The second is         are sets of formula occurrences. We choose to work with the
                 ω                                                             latter presentation because this viewpoint was necessary in a
             µLK , which will serve as an intermediate proof system. At
             the end of this section, we show a sufficient condition that       previous work [8], which is an essential building block for our
             ensures the translatabilty of µLKω proofs into µLK ones.          completeness proof, and for technical reasons that will be clear
             A. Syntax and semantics                                           later in the paper. We present below the notion of occurrence
                                                                               and use it to build µLK and µLKω.
             Definition 1. Let V = {X,Y,...} be a set of variables and             1) Occurrences:
             P = {p,q,...} a set of atoms. The linear-time µ-calculus          Definition 3. An address is a word over {l,r,i}, which stands
             formulas ϕ,ψ,..., called simply formulas, are given by:
                 ϕ::=p|¬p|X |ϕ∨ϕ|ϕ∧ϕ|⊙ϕ|µX.ϕ|νX.ϕ                              for left, right and inside. We denote by ε the empty address.
                                                                               We say that α′ is a sub-address of α when α is a prefix of
             The connectives µ and ν bind the variable X in ϕ. From            α′, written α ⊑ α′. We say that α and β are disjoint when α
             there, bound variables, free variables and capture-avoiding       and β have no upper bound w.r.t. ⊑.
             substitution are defined in a standard way. The subformula         Definition 4. An occurrence (denoted by F, G, H) is given
             ordering is denoted ≤ and fv(•) denotes free variables. Atoms     by a formula ϕ and an address α, and written ϕ . We say
             and their negations are called litterals. We shall use σ to                                                           α
             denote either µ or ν.                                             that two occurrences are disjoint when their addresses are.
                                                                               Let F = ϕ be an occurrence and β an address. We define
                                                                                           α
               Note that we do not allow negations on variables. This is not   F to be ϕ . We say that we relocated F in β. We define F
                                                                                 β        β
             a restriction since we are mostly interested in closed formulas.  to be ϕ. We write F ≡ G if F = G, we say that F and G are
             All the results presented here extend to the general case, where  equal up to renaming. Operations on formulas are extended to
             negations are allowed under a positivity condition on bound       occurrences as follows: for any ⋆ ∈ {∨,∧}, F ⋆G = (ϕ⋆ψ)α
             variables. We do not consider the boolean constants ⊤,⊥ as        if F = ϕ      and G = ψ ; σX.F = (σX.ϕ) and ⊙F =
                                                                                         αl              αr                     α
             they can be encoded by ⊤ := νX.⊙X and ⊥ := µX.⊙X.                 (⊙ϕ) if F = ϕ ; we also allow ourselves to write litterals
                                                                                     α          αi
               The models of our formulas are the ω-words over the             as occurrences without specifying their address. Substitution
                              P
             alphabet Σ := 2 . Intuitively, every position of such a word      of occurrences is defined by (ϕα)[ψβ/X] = (ϕ[ψ/X])α.
                          Formulas with fixed points support two notions of subfor-                                                                Γ,F ⊢ ∆              Γ⊢F,∆ (Cut)                           Γ⊢∆                 (⊙)
                      mula. The first is the usual one: ψ ≤ ϕ if the syntactic tree                                                                             Γ⊢∆                                    Σ⊙Γ⊢Θ,⊙∆
                      of ψ is a sub-tree of the syntactic tree of ϕ. In general, the                                                              F ≡G                             Γ⊢∆                              Γ⊢∆
                                                                                                                                                               (Ax)                             (W)                              (Wr)
                      subformula of a closed formula may contain free variables.                                                                  F ⊢G                           Γ,F ⊢ ∆            l             Γ⊢F,∆
                      The second one is specific to formulas with fixed points, it is
                      a sort of subformula up to unfolding, so that the subformulas                                                               Γ,F ⊢ ∆              Γ,G⊢∆ (∨l)                          Γ⊢F,G,∆ (∨r)
                      of a closed formula w.r.t. this notion are also closed; we call                                                                    Γ,F ∨G⊢∆                                         Γ⊢F∨G,∆
                      it Fischer-Ladner subformula and introduce it below.                                                                          Γ,F,G⊢∆                                   Γ⊢F,∆               Γ⊢G,∆
                      Definition 5. We define the relation → on occurrences as                                                                      Γ,F ∧G⊢∆ (∧l)                                     Γ⊢F∧G,∆                        (∧r)
                      follows, where ⋆ ∈ {∨,∧}:                                                                                                Fig. 1: Inference rules for propositional connectives.
                               (ϕ⋆ψ)α → ϕαl (ϕ⋆ψ)α → ψαr
                               (⊙ϕ)          → ϕ                   (σX.ϕ)            → (ϕ[σX.ϕ/X])                                                  Γ,F[σX.F/X]⊢∆                              Γ⊢F[σX.F/X],∆
                                        α              αi                       α                                    αi                                                               (σ)                                        (σ )
                                                                                                                                                          Γ,σX.F ⊢∆                      l          Γ⊢σX.F,∆                        r
                      A FL-suboccurrence of F is any G such that F →∗ G,
                                      ∗                                                                                                                                                                         ∞
                      where → is the reflexive transitive closure of →. The FL-                                                                Fig. 2: Fixed point rules for the µLK                                  proof system.
                      subformulas of F are obtained by forgetting the adresses of its
                      FL-suboccurrences. The Fischer-Ladner closure of a formula
                      occurrence, denoted FL(F), is the set of its FL-subformulas.                                                     Definition 7. A thread of F is a sequence t = (F )                                               , where
                                                                                                                                                                                                                              i i∈o
                                                                                                                                       o ∈ ω +1 s.t. F = F and ∀i ∈ o, F → F                                               or F = F               .
                      Example 1. Let Φ = µX.νY.⊙X∧⊙Y and Ψ = νY.⊙Φ∨                                                                                                0                                     i          i+1            i         i+1
                                                                                                                                       Let t be the sequence (F )                             i.e., the sequence obtained by
                      ⊙Y. We have for instance:                                                                                                                                     i i∈o
                                                                                                                                       forgetting the adresses of the formula occurrences of t. We
                           Φ →Ψ →(⊙Φ∨⊙Ψ) →(⊙Φ) →Φ →Ψ                                                                                   denote by Inf(t) the elements of t that appear infinitely often
                              ε           i                            ii                 iil           iili           iilii           in t.
                      We have FL(Φε) = {Φ,Ψ,⊙Φ∨⊙Ψ,⊙Ψ,⊙Φ}.                                                                                  A thread t starting from F can be seen as a path in the
                          It is well-known that FL(F) is finite. The FL-suboccurrences                                                  graph G(F). Since t ⊆ FL(F), Inf(t) is finite. The following
                      of F are induced by traversals of the graph of F, i.e., the graph                                                proposition shows that Inf(t) admits a minimum.
                      obtained from the tree of F, by adding the possibility of jump-                                                  Proposition 2. Let t = (F )                                  be a thread of F. The set
                      ing from a variable to the fixed-point combinator introducing                                                                                                       i i∈ω
                      it. This observation is made precise in the following.                                                           Inf(t) admits a minimum w.r.t. ≤, we denote it min(Inf(t)).
                                                                                                                                       Example 3. Let t be the thread of Φε (from Example 1) that
                      Definition 6. The tree of a formula ϕ, denoted τ(ϕ), is                                                                                                                        ⋆                 ⋆
                                                                                                                                       goes to the right: t = Φ → Ψ → Ψ                                          → Ψ                   . . .  We
                      obtained from the syntactic tree of ϕ by labelling every edge                                                                                              ε           i             iiri             iiriiri
                      e as follows: if e is the right (resp. left) outgoing edge of a                                                  have Inf(t) = {Ψ,⊙Φ∧⊙Ψ,⊙Ψ} and min(Inf(t)) = Ψ.
                      binary connective, then it is labelled r (resp. l); otherwise it                                                     We are now ready to introduce our sequent calculus.
                      is labelled i. The graph of a formula ϕ, denoted G(ϕ), is the                                                        2) Circular proof system:
                      rooted graph obtained from τ(ϕ) by identifying the nodes of                                                      Definition 8. A sequent, written ∆ ⊢ Γ, is pair of two finite
                      bound variables with their binders.                                                                              sets of pairwise disjoint occurrences. A pre-proof of µLK∞
                      Example 2. Let Φ be the formula of Example 1. The tree and                                                       is a possibly infinite tree, coinductively generated by the rules
                      the graph of Φ are the following:                                                                                of Figures 1 and 2.
                              τ(Φ)         =         µX                              G(Φ)         =         µX                             The disjointness condition on sequents ensures that two
                                                         i                                                      i                      occurrences from the same side of a given sequent will
                                                     νY                                                     νY                         never engender a common sub-occurrence. Note that if the
                                                                                                   i                                   disjointness condition is satisfied for the conclusion sequent
                                                         i                                                      i                      of a pre-proof, then all its sequents satisfy it, as soon as
                                                       ∧                                                      ∧         i
                                                    l        r                                             l        r                  occurrences of cut-formulas are appropriately chosen [11].
                                               ⊙              ⊙                                       ⊙              ⊙                     Wesometimeswritesequentsoftheformϕ ⊢ ψ asϕ ⊢ ψ.
                                                                                                                                                                                                                      ε         ε
                                                  i              i                                                                         Pre-proofs are unsound: it is easy to derive the formula
                                              X               Y                                                                        µX.⊙X,which is semantically equivalent to ⊥, by applying
                      Proposition 1. Let F = ϕ be an occurrence. If ψ is a FL-                                                         coinductively (µr) rule followed by (⊙) rule. In order to obtain
                                                                    α                                           β                      proper proofs from pre-proofs, we add a validity condition that
                      suboccurrence of F, then β = α.p, where p is a path of G(ϕ)                                                      reflects the nature of our two fixed points.
                      from the root to some node n, denoted N (ψ ).
                                                                                               F      β                                Definition 9. A thread t is said to be a µ-thread (resp. ν-
                          While defining the circular proof system, we will deal with                                                   thread) if min(Inf(t)) is a µ (resp. ν) formula. Let γ = (∆ ⊢
                                                                                                                                                                                                                                              i
                                                                                                                                                                                                                              ∞
                      sequences of occurrences related by →, that we call threads.                                                     Γ )          be an infinite branch in a pre-proof of µLK                                    . A thread
                                                                                                                                          i i∈ω
The words contained in this file might help you see if this file matches what you are looking for:

...Constructive completeness for the linear time calculus amina doumane irif universite paris diderot cnrs fr abstract modal is one of central logics really met since only existing algorithm naive verication in his seminal paper kozen proposed an axiomati that enumerates all lk proofs zation this logic which was proved to be complete years aproof a mathematical argument show later by kaivola case and walukiewicz ing every valid formula provable but it not always branching these are based on complex possible extract from such pro non arguments yielding no reasonable construct formulas problematic duces indeed constructiveness becomes when we consider as may involve certicates supporting answers tools our method actually constructing proof contrary provide new specifying search i e builds readily provides realistic achieve decompose difcult problem into several easier ones taking advantage none correspondence between automata theory w r t s axiomatization more precisely lift well known tran...

no reviews yet
Please Login to review.