, , vol.50, 2018.
, Ob j B , (c 50 , 2019) Ob j B et (c 50 , 2020) Ob j B par définition, vol.50, 2018.
, Chapitre 3. Une extension temporelle pour BI
, Ob j B 2 . Alors, par 7, vol.50, 2018.
, Par 2., 30 cents permettent d'acheter l'objet B l'année prochaine en, 2018.
, Comme 1 euro et 30 cents se composent en moins de 1,50 euros, par 1. et 3. on a que 1,50 euros permettent à la fois d'acheter l'objet A et d'acheter l'objet B l'année prochaine en, 2018.
, Par 5., 1,50 euros permettra d'acheter l'objet C un jour en, 2018.
, 1,50 euros permettent d'acheter à la fois l'objet A et l'objet B l'année prochaine, mais aussi d'acheter un jour l'objet C en, 2018.
, cents permettent d'acheter l'objet B à la fois en, 2018.
, 50 cents permettent toujours d'acheter l'objet B à partir de, 2018.
, On voit ainsi comment l'ajout des opérateurs de LTBI permet de décrire des situations de consommation de ressources qui évoluent dans le temps
, Si T¬? : x ? F , alors F? : x ? F , 7. Si F¬? : x ? F , alors T? : x ? F, vol.6
,
, Si F? ? ? : x ? F , alors F? : x ? F ou F? : x ? F
,
,
,
,
,
, ? ?) ? F , alors T @ x (?) ? F et T @ x (?) ? F
, ? ?) ? F , alors F @ x (?) ? F ou F @ x (?) ? F
, ? ?) ? F , alors F @ x (?) ? F et F @ x (?) ? F
, ? ?) ? F , alors T @ x (?) ? F et F @ x (?) ? F
,
, z ? A(F ) tels que T @ y (?) ? F et F @ z (?) ? F et T @ z (x * y) ? F
,
,
The B-book : assigning programs to meanings, 1996. ,
Trust Domains : An Algebraic, Logical, and Utility-Theoretic Approach, Trust and Trustworthy Computing, TRUST 2013, pp.232-249, 2013. ,
Trust domains in system models : algebra, logic, utility, and combinators, Journal of Logic and Computation, 2015. ,
A calculus and logic of bunched resources and processes, Theoretical Computer Science, vol.614, pp.63-96, 2016. ,
A Road-Map on Complexity for Hybrid Logics, LNCS, vol.1683, pp.307-321, 1999. ,
URL : https://hal.archives-ouvertes.fr/inria-00000337
Gentzen-type systems, resolution and tableaux, Journal of Automated Reasoning, vol.10, issue.2, pp.265-281, 1993. ,
Decidability of Iteration-free PDL with Parallel Composition, Workshop on Automated Deduction : Decidability, Complexity, Tractability, ADDCT'14, 2014. ,
About intuitionistic public announcement logic, 11th conference on Advances in Modal logic, pp.97-116, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01650178
Epistemic actions as resources, Journal of Logic and Computation, vol.17, issue.3, pp.555-585, 2007. ,
Propositional Dynamic Logic with Storing, Recovering and Parallel Composition. Logical and Semantic Frameworks, with Applications Workshop, vol.269, pp.95-107, 2010. ,
Handbook of Logic in Artificial Intelligence and Logic Programming IV : Epistemic and Temporal Reasoning, chapter Temporal Logic, pp.241-350, 1995. ,
A Term Calculus for Intuitionistic Linear Logic, Typed Lambda Calculi and Applications, TLCA '93, vol.664, pp.75-90, 1993. ,
A Separation Logic for Resource Distribution : Extended Abstract, Foundations of Software Technology and Theoretical Computer Science, FST TCS 2003, vol.2914, pp.23-37, 2003. ,
Internalizing labelled deduction, Journal of Logic and Computation, vol.10, issue.1, pp.137-168, 2000. ,
Representation, reasoning, and relational structures : A hybrid logic manifesto, Logic Journal of the IGPL, vol.8, issue.3, 2000. ,
Arthur Prior and Hybrid Logic, Synthese, vol.150, issue.3, pp.329-372, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00119854
Tableau-based Decision Procedures for Hybrid Logic, JLC, vol.16, issue.6, pp.737-763, 2006. ,
Intuitionistic hybrid logic : Introduction and survey. Information and Computation, Intuitionistic Modal Logic and Applications, vol.209, pp.1437-1446, 2008. ,
A Unified Display Proof Theory for Bunched Logic, Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics, vol.265, pp.197-211, 2010. ,
Parametric Completeness for Separation Theories, SIGPLAN Not, vol.49, issue.1, pp.453-464, 2014. ,
Moving Fast with Software Verification, NASA Formal Methods, pp.3-11, 2015. ,
Beiträge zur Begründung der transfiniten Mengenlehre, Mathematische Annalen, vol.46, issue.4, pp.481-512, 1895. ,
Anytime, Anywhere : Modal Logics for Mobile Ambients, pp.365-377, 2000. ,
Typed Multiset Rewriting Specifications of Security Protocols, Electr. Notes Theor. Comput. Sci, vol.40, pp.8-51, 2000. ,
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, pp.52-71, 1981. ,
Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specifications, ACM Trans. Program. Lang. Syst, vol.8, issue.2, pp.244-263, 1986. ,
Model Checking, 1999. ,
A substructural logic for layered graphs, Journal of Logic and Computation, vol.24, issue.4, pp.953-988, 2014. ,
Layered graph logic as an assertion language for access control policy models, Journal of Logic and Computation, vol.27, issue.1, pp.41-80, 2017. ,
A discipline of mathematical systems modelling, 2012. ,
Algebra and logic for resource-based systems modelling. Mathematical Structures in Computer Science, vol.19, pp.959-1027, 2009. ,
Logiques de ressources dynamiques : modèles, propriétés et preuves, 2015. ,
A Public Announcement Separation Logic, Mathematical Structures in Computer Science (MSCS, 2017. ,
A Modal BI Logic for Dynamic Resource Properties, International Symposium LFCS, vol.7734, pp.134-148, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01259770
A modal separation logic for resource dynamics, Journal of Logic and Computation, p.31, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01258982
A logic of separating modalities, Theoretical Computer Science, vol.637, pp.30-58, 2016. ,
An epistemic separation logic, International Workshop on Logic, Language, Information, and Computation, pp.156-173, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01259768
A Hybrid Linear Logic for Constrained Transition Systems, LIPIcs, editor, TYPES'2013, vol.26, pp.150-168, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01285039
Over de sequentialiteit van procesbeschrijvingen. circulated privately, undated, 1962. ,
Dynamic Epistemic Logic, 2007. ,
URL : https://hal.archives-ouvertes.fr/hal-00868361
Intuitionistic layered graph logic, International Joint Conference on Automated Reasoning, pp.469-486, 2016. ,
Relevance Logic and Entailment, pp.117-224, 1986. ,
Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.18, issue.2, pp.194-211, 1979. ,
First-order Logic and Automated Theorem Proving, 1996. ,
A Substructural Epistemic Resource Logic, Indian Conference on Logic and Its Applications, number 10119 in LNCS, pp.106-122, 2017. ,
Semantic Labelled Tableaux for Propositional BI, J. Log. Comput, vol.13, issue.5, pp.707-753, 2003. ,
URL : https://hal.archives-ouvertes.fr/inria-00099556
Characterizing Provability in BI's Pointer Logic through Resource Graphs, Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005, pp.459-473, 2005. ,
Resource Graphs and Countermodels in Resource Logics, ENTCS, vol.125, issue.3, pp.117-135, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00100048
Mathematical Structures in Computer Science, vol.15, pp.1033-1088, 2005. ,
A Linear Logic of Authorization and Knowledge, pp.297-312, 2006. ,
Fast LTL to Büchi Automata Translation, Computer Aided Verification, pp.53-65, 2001. ,
Simple On-the-fly Automatic Verification of Linear Temporal Logic, pp.3-18, 1996. ,
Linear Logic, Theoretical Computer Science, vol.50, pp.1-102, 1987. ,
URL : https://hal.archives-ouvertes.fr/inria-00075966
, Modal Logics and Philosophy. Acumen, 2009.
Logics of Time and Computation. Center for the Study of Language and Information, 1987. ,
Labelled Modal Tableaux, Advances in Modal Logic, vol.7, pp.87-110, 2008. ,
Modeling Adversaries in a Logic for Security Protocol Analysis, pp.115-132, 2003. ,
Dynamic Logic, 2000. ,
Algebraic Laws for Nondeterminism and Concurrency, J. ACM, vol.32, issue.1, pp.137-161, 1985. ,
A Simple Separation Logic, Logic, Language, Information, and Computation, pp.168-178, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01147307
An Axiomatic Basis for Computer Programming, Commun. ACM, vol.12, issue.10, pp.576-580, 1969. ,
A Labelled Sequent Calculus for BBI : Proof Theory and Proof Search, Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013, pp.172-187, 2013. ,
BI as an Assertion Language for Mutable Data Structures, Symposium on Principles of Programming Languages, pp.14-26, 2001. ,
Temporal BI : Proof system, semantics and translations, Theoretical Computer Science, vol.492, pp.40-69, 2013. ,
Temporal Logic and State Systems, Texts in Theoretical Computer Science. An EATCS Series, 2008. ,
The formal strong completeness of partial monoidal Boolean BI, J. Log. Comput, vol.26, issue.2, pp.605-640, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01256932
Exploring the relation between Intuitionistic BI and Boolean BI : an unexpected embedding, Mathematical Structures in Computer Science, vol.19, issue.3, pp.435-500, 2009. ,
URL : https://hal.archives-ouvertes.fr/hal-00577929
The Undecidability of Boolean BI through Phase Semantics, Symposium on Logic in Computer Science, LICS 2010, pp.140-149, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-00577919
Nondeterministic Phase Semantics and the Undecidability of Boolean BI, ACM Trans. Comput. Log, vol.14, issue.1, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01256956
Symbolic logic. Century philosophy series. The Century co, 1932. ,
Intuitionistic LTL and a New Characterization of Safety and Liveness, Computer Science Logic, pp.295-309, 2004. ,
, Preuves et sémantiques dans des logiques de ressources, 2004.
Budget-Constrained Knowledge in Multiagent Systems, Conference on Autonomous Agents and Multiagent Systems, pp.219-226, 2015. ,
The logic of bunched implications, Bulletin of Symbolic Logic, vol.5, issue.2, pp.215-244, 1999. ,
Local Reasoning about Programs that Alter Data Structures, Computer Science Logic, pp.1-19, 2001. ,
Logics of Public Communications, Proc. of the 4 th ISMIS, pp.201-216, 1989. ,
The Temporal Logic of Programs, Foundations of Computer Science, FOCS 1977, pp.46-57, 1977. ,
Prior. Past, Present and Future, 1967. ,
, Papers on Time and Tense, 2003.
The Semantics and Proof Theory of the Logic of Bunched Implications, Applied Logic Series, 2002. ,
Possible worlds and resources : the semantics of BI, Theoretical Computer Science, vol.315, issue.1, pp.257-305, 2004. ,
A Calculus and logic of resources and processes, Formal Asp. Comput, vol.18, issue.4, pp.495-517, 2006. ,
, Systems Modelling via Resources and Processes : Philosophy, Calculus, Semantics, and Logic. ENTCS, vol.172, pp.545-587, 2007.
Specification and verification of concurrent systems in CE-SAR, International Symposium on Programming, pp.337-351, 1982. ,
Relevant Logic : A Philosophical Examination of Inference, 1988. ,
An Introduction to Substructural Logics. Routledge, 2000. ,
Separation logic : a logic for shared mutable data structures, Proc. 17 th Annual IEEE Symp. Logic in Computer Science, pp.55-74, 2002. ,
, The weakest link, 2005.
Internalization : The case of hybrid logics, Journal of logic and computation, vol.11, issue.5, pp.671-689, 2001. ,
Models and Languages for Parallel Computation, ACM Comput. Surv, vol.30, issue.2, pp.123-169, 1998. ,
A Spatial-Epistemic Logic for Reasoning about Security Protocols, Security Issues in Concurrency, vol.51, pp.1-15, 2010. ,
Handbook of epistemic logic, 2015. ,
Si T?? : (x, u) ? F , alors ?l ? L s \ A s (C s ), F ? {T? : (x, l)}, C r , C s ? {u l}} ? P 20'. Si F? : (x, u) ? F , alors ?l ? L s \ A s (C s ), F ? {F? : (x, l)}, C r , C s ? {u l}} ? P 21' Si T?? : (x, u) ? F , alors ?l ? L s \ A s (C s ), F ? {T? : (x, l)}, C r , C s ? {u l}} ? P 22' Si F?? : (x, u) ? F , alors ?l ? L s \ A s (C s ), F ? {F?, 25 Years of Model Checking -History, Achievements, Perspectives, vol.5000, pp.150-171, 2008. ,
, Proposition A.1. L'ensemble de tous les CTSS finis pour lesquels il n'existe pas de LTBI
ensemble de tous les CTSS finis pour lesquels il n'existe pas de LTBI-tableau clos. On montre que P est une propriété de consistance ,
,
Par la règle TI, [F , C r ? {1 r x}, C s ] est un LTBItableau pour F , C r , C s . Donc F , C r , C s a un tableau clos ,
, T? : (x, u)}, C r , C s ? P . Par la règle T?, Si T? ? ? : (x, u) ? F . On suppose que F ? {T? : (x, u)
C s a un LTBI-tableau clos, ce qui est contradictoire, Donc F ? {T? : (x, u), T? : (x, u) ,
,
On suppose que F ? {F? ,
C s a un LTBI-tableau clos, ce qui est contradictoire ,
, F? : (c, u)}, C r ? {x c}, C s ] est un LTBI-tableau pour F , C r , C s . Donc F , C r , C s a un LTBI-tableau clos, Si F? ? ? : (x, u) ? F . On choisit c ? ? r \ A r (C r ) (notons que ? r est infini et A r (C r ) est fini car C r est fini)
On choisit l ? L s \ A s (C s ) (notons que L s est infini et A s (C s ) est fini car C s est fini) ,
C s a un LTBI-tableau clos, ce qui est contradictoire. Donc F ? {T? : (x, l), C r , C s ? {u l}} ? P ,
On suppose que F ? {F? : (x, l) ,
,
F? : (y, u)}, C r f , C s f f F , C r , C s . On remarque par le Corollaire 3.1 que ce CTSS satisfait (P CSS ), On suppose que T? : (x, u) ? F et F? : (y, u) ? F et x y ? C r . Par (P CSS ) ,
Par (P CSS ), u u ? C s . En outre, il existe deux labels y et z tels que yz x ? C r et T? : (y, u) ? F . Par compacité (Lemme 3.4), il existe C r f ? C r et C s f ? C s tels que C r f et C s f soient finis ,
,
,
, A r (C ri ) ? {1 r , c 1 , c 2, p.2
C s? est clos. Alors, par définition d'un oracle, i+1 } Démonstration. 1. On suppose que T? : (x, u) ,
, Similaire à la condition 1
, Similaire à la condition 1
, Similaire à la condition 1
, Similaire à la condition 1
, Comme la suite F i , C ri , C si 0i est croissante (propriété 2 de la Proposition 3.6), on a TI : (x, u) ? F k . Par la propriété 3 de la Proposition 3.6, F k , C rk , C sk ? P . Donc F k+1 , C rk+1 , C sk+1 = F k
T? : (x, u)}, C r? , C s? ? P par la règle T?, On suppose que T? ? ? : (x, u) ? F ? . Comme P est saturé, on a F ? ? {T? : (x, u) ,
s? ? P par la règle F?. Par la propriété 2 de la Propo ,
, Similaire à la condition 8
, Similaire à la condition 7
, On suppose que T? ? ? : (x, u)
On suppose que T? * ? : (x, u) ? F ? . Par un argument similaire à celui de la condition 6, il existe k ? N tel que : -le k ième élément de notre stratégie équitable, On suppose que F? ? ? : (x, u) ? F ? . Par un argument similaire à celui de la condition 6, il existe k ? N tel que : -le k ième élément de notre stratégie équitable est F? ? ? : (x, u) -F? ? ? : (x, u) ,
On suppose que F? * ? : (x, u) ? F ? . Soit c, d ? L r tel que cd x ? C r?, T? : (b, u) ,
, Similaire à la condition 11
, Similaire à la condition 12
Par un argument similaire à celui de la condition 6, il existe k ? N tel que : -le k ième élément de notre stratégie équitable est T?? : (x, u) -T?? : (x, u) ,
,
Soit l ? L s tel que u l ? C s? . Comme P est saturé, on a F ? ? {F? : (x, l)}, C r? , C s? ? P par la règle F? ,
, Similaire à la condition 18
, Similaire à la condition 17
, Similaire à la condition 17
, Similaire à la condition 17
C s? ? {w v}} ? P par la règle . Alors, par la propriété 3 de la Proposition ,
,
, Parmi tous les TPN C tels que (C,C ) ? E (c'est à dire les fils de C), au moins un est réalisable et le modèle
alors C a été étendu par une règle de la figure 3.12. On montre que quelque soit la règle, au moins un des TPN obtenus est réalisable ,
On note R = (K , ., s) la réalisation de C ,
,
, -I ? ou ? ou ou Dans ces cas là, d'après le Lemme 3.20, C n'est pas réalisable. Ces cas ne sont donc pas possibles
et donc par définition (x, s) K I. Alors par la Définition 3, Donc R est une réalisation du nouveau TPN F + \ {I : x}, F ? , C r ? {1 r x}}, vol.4 ,
Alors par définition, on a (x, s) K A ? B. Donc par la Définition 3.4, on a (x, s) K A et (x, s) K B. Donc R est une réalisation du nouveau ,
Alors par définition, on a (x, s) K A ? B. Donc par la Définition 3.4, on a (x, s) K A ou (x, s) K B. Donc R est une réalisation d'un des nouveaux, x}\{A?B : x}, C r et F + , F ? ?{B : x}\{A?B : x}, C r , qui sont les deux seuls fils de C ,
Alors par définition, on a (x, s) K A ? B. Donc par la Définition 3.4, on a (x, s) K A ou (x, s) K B. Donc R est une réalisation d'un des nouveaux TPN F + ?{A : x}\{A?B : x}, x}\{A?B : x}, F ? , C r , qui sont les deux seuls fils de C ,
Alors par définition, on a (x, s) K A ? B. Donc par la Définition 3.4, on a (x, s) K A et (x, s) K B. Donc R est une réalisation du ,
Alors par définition, et par le Lemme 3.21, on a (x, s) K A ? B et x y. Donc par la Définition 3.4, on a que si (y, s) K A, alors (y, s) K B, c'est à dire que (y, s) K A ou (y, s) K B Donc R est une réalisation d'un des nouveaux ,
Donc par la Définition 3.4, il existe r ? R tel que x r et (r, s) K A et (r, s) K B. Comme c i est un nouveau label de ressources, c i n'est pas défini. On peut donc étendre . en posant c i = r. Alors cette extension de R est une réalisation du nouveau ,
Alors par définition, on a (x, s) K A * B. Donc par la Définition 3.4, il existe r 1 , r 2 ? R tel que r 1 ? r 2 x et (r 1 , s) K A et ,
, On peut donc étendre . en posant c i = r 1 et c j = r 2 . Alors cette extension de R est A.6
,
Alors par définition, et par le Lemme 3.21, on a (x, s) K A * B et y ? z x. Donc par la Définition 3.4, on a (y, s) K A ou (z, s) K B. Donc R est une réalisation d'un des nouveaux ,
Alors par définition, et par le Lemme 3.21, on a (x, s) K A ? * B et x ? y x ? y. Donc par la Définition 3.4, on a que si (y, s) K A, alors (x?y, s) K B, c' ,
,
Alors par définition, on a (x, s) K A. Alors par le Lemme 3.3, on a aussi (x, s) K A ? ?A. Donc par la Définition 3.4, on a (x, s) K A et (x, s) K ?A. Donc R est une réalisation du nouveau TPN F + ? {A : x, ?A : x} \ {A : x}, F ? , C r , qui est l'unique fils de C. -? Dans ce cas A : x ? F ? . Alors par définition, on a (x, s) K A. Alors par le Lemme 3.3, on a aussi (x, s) K A ? ?A. Donc par la Définition 3.4, on a (x, s) K A ou (x, s) K ?A. Donc R est une réalisation d'un des nouveaux, Donc par la Définition 3.4, il existe r ? R tel que (r, s) ,
Alors par définition, on a (x, s) K ?A. Alors par le Lemme 3.3, on a aussi (x, s) K A ? ??A. Donc par la Définition 3.4, on a (x, s) K A ou (x, s) K ??A. Donc R est une réalisation d ,
,
Alors par définition, on a (x, s) K ?A. Alors par le Lemme 3.3, on a aussi (x, s) K A ? ??A. Donc par la Définition 3.4, on a (x, s) K A et (x, s) K ??A. Donc R est une réalisation du ,
, Annexe B. Preuves du Chapitre, vol.5
, Alors on a T @ x (? ? ?) ? F . Comme F est réalisable, on a x K ? ? ?, ce qui veut dire que ou bien x K ?, ou bien x K ?. Alors K est une réalisation d'au moins une des deux nouvelles branches F ? {F @ x (?)} et F ? {T @ x (?)} et T reste réalisable
Alors K est une réalisation de la nouvelle branche F ? {T @ x (?), F @ x (?)} et T reste réalisable. -T¬ Alors on a T @ x (¬?) ? F . Comme F est réalisable, on a x K ¬?, ce qui veut dire que x K ?. Alors K est une réalisation de la nouvelle branche F ? {F @ x (?)} et T reste réalisable, Alors on a F @ x (¬?) ? F . Comme F est réalisable, on a x K ¬?, ce qui veut dire que x K ?. Alors K est une réalisation de la nouvelle branche F ? {T @ x (?)} et T reste réalisable. -T * * Alors on a T @ x (? * ?) ? F . Comme F est réalisable, on a x K ? * ? ce qui veut dire qu ,
, T @ c j (?), T @ x (c i * c j )} et T reste réalisable. -F * * Alors on a F @ x (? * ?) ? F et T @ x (y * z) ? F . Comme F est réalisable, on a x K ? * ? et x K y * z. Ce dernier point nous indique par le premier point du Lemme 5.1 que y ? z ? et x ? y ? z. Or, comme x K ? * ?, pour tout r, r ? Nom on a ou bien r ? r ?, ou bien x ? r ? r ou bien r K ?, ou bien r K ?. Comme y ? z ? et x ? y ? z
Ce dernier point nous indique par le premier point du Lemme 5.1 que x ? y ? et z ? x ? y. Or, comme x K ? ? * ?, pour tout r ? Nom tel que x ? r ? et r K ?, on a x ? r K ? . Comme x ? y ?, on a donc pour r = y que si y K ?, alors x ? y K ?. On a donc ou bien y K ?, ou bien x ? y K ?, ce deuxième cas, par monotonie et comme z ? x ? y on a aussi z K ?. Finalement, K est une réalisation d'au moins une des deux nouvelles branches F ? {F @ y (?)} et F ? {T @ z (?)} et T reste réalisable ,
, Alors on a F @ x (? ? * ?) ? F . Comme F est réalisable
l'absence de c i et c j dans F assure que le modèle identique à K sauf concernant c i et c j est aussi une réalisation de F et on peut travailler avec celui-ci sans perte de validité de notre raisonnement ,
, Une propriété de consistance est un ensemble P de SHS qui satisfait les conditions suivante pour tout F ? P
,
,
F ) tel que c i = c j et F ? {T @ c i (?), F @ c j (?) T @ c j (x * c i )} ? P ,
,
,
, T @ c i (y * z)} ? P pour toute substitution
, T @ c i (y * z)} ? P pour toute substitution
,
,
, Annexe B. Preuves du Chapitre, vol.5
, On étend la notion de substitution aux formules étiquetées par : ?(S @ x (?)) = S @ ?(x) (?(?))
, On étend la notion de substitution à toute branche F par : ?(F ) = {?(S @ x (?))|S @ x (?) ? F } Proposition B.3. Pour toute substitution ?, on a : ?(F ) ? {?(S @ x (?))} = ?(F ? {S @ x (?)})
,
, Proposition B.4. Pour toute substitution ?
, Si F f est un SHS fini, alors ?(F ) est un SHS fini
, alors ?(F ) ? ?(F )
La preuve est directe étant donné que |?(F ) ,
Par définition de ?, F est de la forme ?(S @ x (?)) avec S @ x (?) ? F . Comme F ? F , on a S @ x (?) ? F , donc ?(S @ x (?)) ? ?(F ), c ,
, Proposition B.5. Toute propriété de consistance ?-close peut être étendue en une propriété de consistance ?-close alternée
,
} ? P , donc par saturation par la règle i+ ,
T @ a (y * z)} ? P , c'est à dire que F i+1 ? P , d'où ]), alors A(F i+1 ) = A(F i ) ? {c 2i+2 }. Or, par (HR), on a A(F i ) ? Nom e ?{c 1 ,
,
} ? P , donc par saturation par la règle i+ ,
, T @ a (y * z)} ? P , c'est à dire que F i+1 ? P , d'où
, A(F i+1 ) = A(F i ) et le point 4. est évident. En outre, par hypothèse, F i ? {F i } ? P par hypothèse
, On donne ici la preuve du Lemme 5.15. Il s'agit d'étendre chacune des définitions et propositions de la Section B.3. On étend d'abord la notion de propriété de consistance
, Une propriété de consistance pour HBBI est un ensemble P de SHS qui satisfait toutes les conditions de la Définition B.1 ainsi que les points additionnels suivants
,
, La notion de propriété de consistance alternée est étendue par les mêmes conditions
, Propriété de consistance alternée pour HBBI -extension de la Définition B.2), Définition B, vol.5
, Une propriété de consistance alternée pour HBBI est un ensemble P de SHS qui vérifie les conditions d'une propriété de consistance alternée (Définition B.2) ainsi que les trois conditions additionnelles de la Définition B.4. On a ensuite les Propositions suivantes, identiques à leurs versions de la Section B.3 : Proposition B.7. L'ensemble de tous les SHS finis pour lesquels il n
, On montre que P est une propriété de consistance. Les conditions 1. à 30. sont prouvées comme dans la preuve de la Proposition B.1. Les points 31. à 33, Soit P l'ensemble de tous les SHS finis pour lesquels il n'existe pas de tableau clos
, Annexe B. Preuves du Chapitre, vol.5
, Comme ?(F ) ? P et que P est une propriété de consistance, par le point 31 de la Défini-tion B.1, on a ?(F ) ? {T @ ?(x) (?(x) * I)} ? P , c'est à dire que ?(F ) ? {T @ ?(x) (?(x) * ?(I))} ? P , c'est à dire que ?(F ) ? {?(T @ x (x * I))} ? P , c'est à dire que ?(F ? {T @ x (x * I)}) ? P (d'après la Proposition B.2), se montre comme dans la preuve de la Proposition B.5. Les points 31. à 33. sont montrés cidessous : 31
, Comme ?(F ) ? P et que P est une propriété de consistance, par le point 32 de la Définition B.1, on a ?(F ) ? {T @ ?(x) (?(z) * ?(y))} ? P , c'est à dire que ?(F ) ? {?(T @ x (z * y))} ? P , c'est à dire que ?(F ? {T @ x (z * y)}) ? P (d'après la Proposition B.2), * z)) ? ?(F )
, Comme ?(F ) ? P et que P est une propriété de consistance, par le point 33 de la Définition B.1, on a ?(F )?{T @ ?(x) ((?(y) * ?(z)) * ?(t))} ? P , c'est à dire que ?(F ) ? {?(T @ x ((y * z) * t))} ? P , c'est à dire que ?(F ? {T @ x ((y * z) * t)}) ? P (d'après la Proposition B.2)
, Toute propriété de consistance ?-close alternée peut être étendue en une propriété de consistance ?-close alternée de caractère fini
, si T est clos, ?(T ) peut être étendu
, On démontre ce résultat pour tous les tableaux par récurrence sur la taille n de T -Cas de base
{F @ c 1 (?)}. C'est un HBBI-tableau pur à un seul SHS pour la formule ?. Donc la propriété est vraie pour tous les BBI-tableaux de taille 1. -Hérédité On suppose la propriété est vraie pour tous les BBI-tableaux de taille n (HR) ,
,
, x ? F . Alors, par construction, on a ?(T ) = ?(T a ) ? ?(F , C ) ? ?(T b ) et ?(F , C ) = F et T @ x (? ? ?) ? F . On a alors T = T a ? F ? {T? : x, T? : x}, C ? T b , et donc ?(T ) = ?(T a ) ? F ? {T @ x (?), T @ x (?)} ? ?(T b )
, Comme ?(T ) est un tableau par (HR), ?(T ) l'est aussi par application de la règle T? à ?(T )
, ? ?) ? F et T @ c (d(x)) ? F . On peut alors choisir à nouveau c pour construire ?(T ) à partir de x et on a ?(T ) = ?(T a ) ? F ? {T @ c (?), T @ c (?), T @ c (d(x))} ? ?(T b )
, x ? F . Alors, par construction, on a ?(T ) = ?(T a ) ? ?(F , C ) ? ?(T b ) et ?(F , C ) = F et F @ x (? ? ?) ? F . On a alors T = T a ? F ? {F? : x}, C
,
, ? ?(T b ). Comme ?(T ) est un tableau par (HR), ?(T ) l'est aussi par application de la règle F? à ?(T )
, ? ?) ? F et T @ c (d(x)) ? F . On peut alors choisir à nouveau c pour construire ?(T ) à partir de x et on a ?(T ) = ?(T a ) ? F ? {F @ c (?)
T @ c (d(x))} ? ?(T b ) ce qui correspond à nouveau à l'application de la règle F? ,
, x ? F . Alors, par construction, on a ?(T ) = ?(T a ) ? ?(F , C ) ? ?(T b ) et ?(F , C ) = F et T @ x (? * ?) ? F . On a alors T = T a ? F ? {T? : c i
, Comme ?(T ) est un tableau par (HR), ?(T ) l'est aussi par application de la règle T * * à ?(T )
, * ?) ? F et T @ c (d(x)) ? F . On peut alors choisir à nouveau c pour construire ?(T ) à partir de x et on a ?(T ) = ?(T a )?F ?{T @ c i (?), T @ c j (?), T @ c (c i * c j ), T @ c (d(x))} ??(T b )
Alors, par construction, on a ?(T ) = ?(T a )??(F , C )??(T b ) et ?(F , C ) = F et F @ x (? * ?) ? F . En outre, comme x yz ? Req et que ?(x yz) ? R (x yz), on a par construction que ?(x yz) ? F , c'est à dire que T @ x (d(y) * d(z)) ? F , c'est à dire T @ x (y * z) ? F si y et z sont non composés, On a alors T = T a ?F ?{F? : y}, C ; F ?{F? : z}, C ?T b ,
,
, Comme ?(T ) est un tableau par (HR), ?(T ) l'est aussi par application de la puis T @ u (?) par i t et i s . D'un autre côté, on peut produire par une série d'application des règles i+ et i? les formules T @ t (w) et T @ w (d(y)) (par T @ t (d(y))) ainsi que T @ u (w) et T @ w (d(y)) (par T @ u (d(y))). On produit alors T @ w (u)
, Si x est composé, ?(x ?) = {T @ y (I), T @ y (d(x))}, F @ z (I) ? F et T @ z (d(x)) ? F . Alors on peut produire par une série d'application des règles i+ et i? les formules T @ y (t) et T @ t (d(x)) (par T @ y (d(x))) ainsi que T @ z (t) et T @ t (d(x)) (par T @ z (d(x))). Alors deux applications de i s et i t produisent T @ t (I) et F @ t (I)
, T? : x ? F . Alors T @ x (?) ? F et F est clos, ou bien T @ y (?) ? F et T @ y (d(x)) ? F et F est clos
, Dans tous les cas, F est étendu en une branche close
Il existe alors un SHS de T , F tel que ?(F ) = F , C . Par hypothèse, F est clos, On a alors 3 cas : -T @ x (?) ? F et F @ x (?) ? F . On a deux cas : -x est un label simple de T . Alors on doit avoir T? : x ? F et F? : x ? F . En outre ,
, -x a été introduit par une règle i+. Comme x est le même dans les deux règles, il doit exister un label composé y tel que T @ x (d(y)) ? F et on a T? : y ? F et F? : y ? F . Par le même raisonnement on a alors F , C clos
, On a alors T? : x ? F , ou alors il existe un label composé y tel que T @ x (d(y)) ? F et on a T? : y ? F . Dans les deux cas
, On a alors F : x ? F , ou alors il existe un label composé y tel que T @ x (d(y)) ? F et on a F : y ? F . Dans les deux cas
Comme ceci est vrai pour tout CSS, T est clos ,