A. , , 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-ti-:-x-?-f-,-alors-x-?-?-c, Si T¬? : x ? F , alors F? : x ? F , 7. Si F¬? : x ? F , alors T? : x ? F, vol.6

S. T?-?-?-:-x-?-f and . T?,

, Si F? ? ? : x ? F , alors F? : x ? F ou F? : x ? F

S. T?-?-?-:-x-?-f and . T?,

S. F?-?-?-:-x-?-f and . F?,

S. T?-?-?-:-x-?-f and . F?,

S. F?-?-?-:-x-?-f and . T?,

S. T?-*-?-:-x-?-f, ?. L-r-,-x-yz-?-c-et-t?-:-y-?-f, and . T?,

. Si-t-@-x, ? ?) ? F , alors T @ x (?) ? F et T @ x (?) ? F

. Si-f-@-x, ? ?) ? F , alors F @ x (?) ? F ou F @ x (?) ? F

. Si-f-@-x, ? ?) ? F , alors F @ x (?) ? F et F @ x (?) ? F

. Si-f-@-x, ? ?) ? F , alors T @ x (?) ? F et F @ x (?) ? F

. Si-f-@-x,

. Si-f-@-x-(?-?-*-?)-?-f, z ? A(F ) tels que T @ y (?) ? F et F @ z (?) ? F et T @ z (x * y) ? F

?. ,

. ?-f-@-c-;-b-?-*-c)-*-d,

J. R. , The B-book : assigning programs to meanings, 1996.

G. Anderson, M. Collinson, and D. J. Pym, Trust Domains : An Algebraic, Logical, and Utility-Theoretic Approach, Trust and Trustworthy Computing, TRUST 2013, pp.232-249, 2013.

G. Anderson and D. Pym, Trust domains in system models : algebra, logic, utility, and combinators, Journal of Logic and Computation, 2015.

G. Anderson and D. Pym, A calculus and logic of bunched resources and processes, Theoretical Computer Science, vol.614, pp.63-96, 2016.

C. Areces, P. Blackburn, and M. Marx, A Road-Map on Complexity for Hybrid Logics, LNCS, vol.1683, pp.307-321, 1999.
URL : https://hal.archives-ouvertes.fr/inria-00000337

A. Avron, Gentzen-type systems, resolution and tableaux, Journal of Automated Reasoning, vol.10, issue.2, pp.265-281, 1993.

P. Balbiani and J. Boudou, Decidability of Iteration-free PDL with Parallel Composition, Workshop on Automated Deduction : Decidability, Complexity, Tractability, ADDCT'14, 2014.

P. Balbiani and D. Galmiche, About intuitionistic public announcement logic, 11th conference on Advances in Modal logic, pp.97-116, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01650178

A. Baltag, B. Coecke, and M. Sadrzadeh, Epistemic actions as resources, Journal of Logic and Computation, vol.17, issue.3, pp.555-585, 2007.

M. R. Benevides, R. De-freitas, and P. Viana, Propositional Dynamic Logic with Storing, Recovering and Parallel Composition. Logical and Semantic Frameworks, with Applications Workshop, vol.269, pp.95-107, 2010.

J. Benthem, Handbook of Logic in Artificial Intelligence and Logic Programming IV : Epistemic and Temporal Reasoning, chapter Temporal Logic, pp.241-350, 1995.

P. N. Benton, G. M. Bierman, V. De-paiva, and M. Hyland, A Term Calculus for Intuitionistic Linear Logic, Typed Lambda Calculi and Applications, TLCA '93, vol.664, pp.75-90, 1993.

N. Biri and D. Galmiche, 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.

P. Blackburn, Internalizing labelled deduction, Journal of Logic and Computation, vol.10, issue.1, pp.137-168, 2000.

P. Blackburn, Representation, reasoning, and relational structures : A hybrid logic manifesto, Logic Journal of the IGPL, vol.8, issue.3, 2000.

P. Blackburn, Arthur Prior and Hybrid Logic, Synthese, vol.150, issue.3, pp.329-372, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00119854

T. Bolander and T. Braüner, Tableau-based Decision Procedures for Hybrid Logic, JLC, vol.16, issue.6, pp.737-763, 2006.

T. Braüner, Intuitionistic hybrid logic : Introduction and survey. Information and Computation, Intuitionistic Modal Logic and Applications, vol.209, pp.1437-1446, 2008.

J. Brotherston, 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.

J. Brotherston and J. Villard, Parametric Completeness for Separation Theories, SIGPLAN Not, vol.49, issue.1, pp.453-464, 2014.

C. Calcagno, D. Distefano, J. Dubreil, D. Gabi, P. Hooimeijer et al., Moving Fast with Software Verification, NASA Formal Methods, pp.3-11, 2015.

G. Cantor, Beiträge zur Begründung der transfiniten Mengenlehre, Mathematische Annalen, vol.46, issue.4, pp.481-512, 1895.

L. Cardelli and A. Gordon, Anytime, Anywhere : Modal Logics for Mobile Ambients, pp.365-377, 2000.

I. Cervesato, Typed Multiset Rewriting Specifications of Security Protocols, Electr. Notes Theor. Comput. Sci, vol.40, pp.8-51, 2000.

E. M. Clarke and E. A. Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, pp.52-71, 1981.

E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specifications, ACM Trans. Program. Lang. Syst, vol.8, issue.2, pp.244-263, 1986.

E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking, 1999.

M. Collinson, K. Mcdonald, and D. Pym, A substructural logic for layered graphs, Journal of Logic and Computation, vol.24, issue.4, pp.953-988, 2014.

M. Collinson, K. Mcdonald, and D. Pym, 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.

M. Collinson, B. Monahan, and D. Pym, A discipline of mathematical systems modelling, 2012.

M. Collinson and D. Pym, Algebra and logic for resource-based systems modelling. Mathematical Structures in Computer Science, vol.19, pp.959-1027, 2009.

J. Courtault, Logiques de ressources dynamiques : modèles, propriétés et preuves, 2015.

J. Courtault, H. V. Ditmarsch, and D. Galmiche, A Public Announcement Separation Logic, Mathematical Structures in Computer Science (MSCS, 2017.

J. Courtault and D. Galmiche, 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

J. Courtault and D. Galmiche, A modal separation logic for resource dynamics, Journal of Logic and Computation, p.31, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01258982

J. Courtault, D. Galmiche, and D. Pym, A logic of separating modalities, Theoretical Computer Science, vol.637, pp.30-58, 2016.

J. Courtault, H. Van-ditmarsch, and D. Galmiche, An epistemic separation logic, International Workshop on Logic, Language, Information, and Computation, pp.156-173, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01259768

J. Despeyroux and K. Chaudhuri, 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

E. W. Dijkstra, Over de sequentialiteit van procesbeschrijvingen. circulated privately, undated, 1962.

H. V. Ditmarsch, W. Van-der-hoek, and B. Kooi, Dynamic Epistemic Logic, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00868361

S. Docherty and D. Pym, Intuitionistic layered graph logic, International Joint Conference on Automated Reasoning, pp.469-486, 2016.

J. M. Dunn, Relevance Logic and Entailment, pp.117-224, 1986.

M. J. Fischer and R. E. Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.18, issue.2, pp.194-211, 1979.

M. Fitting, First-order Logic and Automated Theorem Proving, 1996.

D. Galmiche, P. Kimmel, and D. Pym, A Substructural Epistemic Resource Logic, Indian Conference on Logic and Its Applications, number 10119 in LNCS, pp.106-122, 2017.

D. Galmiche and D. Méry, 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

D. Galmiche and D. Méry, Characterizing Provability in BI's Pointer Logic through Resource Graphs, Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005, pp.459-473, 2005.

D. Galmiche and D. Méry, Resource Graphs and Countermodels in Resource Logics, ENTCS, vol.125, issue.3, pp.117-135, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00100048

D. Galmiche, D. Méry, and D. Pym, Mathematical Structures in Computer Science, vol.15, pp.1033-1088, 2005.

D. Garg, L. Bauer, K. D. Bowers, F. Pfenning, and M. K. Reiter, A Linear Logic of Authorization and Knowledge, pp.297-312, 2006.

P. Gastin and D. Oddoux, Fast LTL to Büchi Automata Translation, Computer Aided Verification, pp.53-65, 2001.

R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper, Simple On-the-fly Automatic Verification of Linear Temporal Logic, pp.3-18, 1996.

J. Girard, Linear Logic, Theoretical Computer Science, vol.50, pp.1-102, 1987.
URL : https://hal.archives-ouvertes.fr/inria-00075966

R. Girle, Modal Logics and Philosophy. Acumen, 2009.

R. Goldblatt, Logics of Time and Computation. Center for the Study of Language and Information, 1987.

G. Governatori, Labelled Modal Tableaux, Advances in Modal Logic, vol.7, pp.87-110, 2008.

J. Y. Halpern and R. Pucella, Modeling Adversaries in a Logic for Security Protocol Analysis, pp.115-132, 2003.

D. Harel, J. Tiuryn, and D. Kozen, Dynamic Logic, 2000.

M. Hennessy and R. Milner, Algebraic Laws for Nondeterminism and Concurrency, J. ACM, vol.32, issue.1, pp.137-161, 1985.

A. Herzig, A Simple Separation Logic, Logic, Language, Information, and Computation, pp.168-178, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01147307

C. A. Hoare, An Axiomatic Basis for Computer Programming, Commun. ACM, vol.12, issue.10, pp.576-580, 1969.

Z. Hou, A. Tiu, and R. Goré, 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.

S. S. Ishtiaq and P. W. O'hearn, BI as an Assertion Language for Mutable Data Structures, Symposium on Principles of Programming Languages, pp.14-26, 2001.

N. Kamide, Temporal BI : Proof system, semantics and translations, Theoretical Computer Science, vol.492, pp.40-69, 2013.

F. Kröger and S. Merz, Temporal Logic and State Systems, Texts in Theoretical Computer Science. An EATCS Series, 2008.

D. Larchey-wendling, 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

D. Larchey-wendling and D. Galmiche, 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

D. Larchey-wendling and D. Galmiche, 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

D. Larchey-wendling and D. Galmiche, 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

C. Lewis and C. Langford, Symbolic logic. Century philosophy series. The Century co, 1932.

P. Maier, Intuitionistic LTL and a New Characterization of Safety and Liveness, Computer Science Logic, pp.295-309, 2004.

D. Méry, Preuves et sémantiques dans des logiques de ressources, 2004.

P. Naumov and J. Tao, Budget-Constrained Knowledge in Multiagent Systems, Conference on Autonomous Agents and Multiagent Systems, pp.219-226, 2015.

P. W. O'hearn and D. J. Pym, The logic of bunched implications, Bulletin of Symbolic Logic, vol.5, issue.2, pp.215-244, 1999.

P. W. O'hearn, J. C. Reynolds, and H. Yang, Local Reasoning about Programs that Alter Data Structures, Computer Science Logic, pp.1-19, 2001.

J. A. Plaza, Logics of Public Communications, Proc. of the 4 th ISMIS, pp.201-216, 1989.

A. Pnueli, The Temporal Logic of Programs, Foundations of Computer Science, FOCS 1977, pp.46-57, 1977.

A. N. , Prior. Past, Present and Future, 1967.

A. N. Prior, Papers on Time and Tense, 2003.

D. Pym, The Semantics and Proof Theory of the Logic of Bunched Implications, Applied Logic Series, 2002.

D. J. Pym, P. W. O'hearn, and H. Yang, Possible worlds and resources : the semantics of BI, Theoretical Computer Science, vol.315, issue.1, pp.257-305, 2004.

D. J. Pym and C. M. Tofts, A Calculus and logic of resources and processes, Formal Asp. Comput, vol.18, issue.4, pp.495-517, 2006.

D. J. Pym and C. M. Tofts, Systems Modelling via Resources and Processes : Philosophy, Calculus, Semantics, and Logic. ENTCS, vol.172, pp.545-587, 2007.

J. P. Queille and J. Sifakis, Specification and verification of concurrent systems in CE-SAR, International Symposium on Programming, pp.337-351, 1982.

S. Read, Relevant Logic : A Philosophical Examination of Inference, 1988.

G. , An Introduction to Substructural Logics. Routledge, 2000.

J. C. Reynolds, Separation logic : a logic for shared mutable data structures, Proc. 17 th Annual IEEE Symp. Logic in Computer Science, pp.55-74, 2002.

B. Schneier, The weakest link, 2005.

J. Seligman, Internalization : The case of hybrid logics, Journal of logic and computation, vol.11, issue.5, pp.671-689, 2001.

D. B. Skillicorn and D. Talia, Models and Languages for Parallel Computation, ACM Comput. Surv, vol.30, issue.2, pp.123-169, 1998.

B. Toninho and L. Caires, A Spatial-Epistemic Logic for Reasoning about Security Protocols, Security Issues in Concurrency, vol.51, pp.1-15, 2010.

H. Van-ditmarsch, J. Y. Halpern, W. W. Van-der-hoek, and B. P. Kooi, Handbook of epistemic logic, 2015.

M. Y. Vardi, 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

. Soit and F. Soit, 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

S. T?-;-x,-u)-?-f-et-f?-;-y,-u)-?-f-et-x-y-?-c-r-alors-le and C. Donc-[f-,-c-r,

S. Ti-;-x and ). , 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)

F. Donc and . R-;-},-c-r-,-c-s-?-p, C s a un LTBI-tableau clos, ce qui est contradictoire, Donc F ? {T? : (x, u), T? : (x, u)

S. F?-?-?-;-x,-u)-?-f-.-on-suppose-que-f-?-{f?-;-x,-u)},-c-r-,-c-s-?-p-et-f-?-{f?-;-x,-u)},-c-r-,-c-s-?-p-.-par-la-règle, F. , and [. F-?-{f?-;-x,-u)},-c-r-,-c-s-;-f-?-{f?,

S. T?-?-?-;-x,-u)-?-f-.-soit-c-?-l-r-tel-que-x-c-?-c-r-;-c,-u)},-c-r-,-c-s-?-p-et-f-?-{t?-;-},-c-r-,-c-s-?-p-.-par-la-règle, T. ??, and [. {f?, On suppose que F ? {F?

F. F-?-{t?-;-c,-u)},-c-r-,-c-s-]-est-un-ltbi-tableau-pour, F. Alors, and C. R-;-},-c-r-,-c-s-?-p-ou-f-?-{t?, 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)

). Si-t??-;-x, 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)

F. Donc, C s a un LTBI-tableau clos, ce qui est contradictoire. Donc F ? {T? : (x, l), C r , C s ? {u l}} ? P

[. Si-f??-;-x,-u)-?-f-.-soit-l-?-l-s-tel-que-u-l-?-c-u-;-},-c-r-,-c-s-?-p-.-par-la-règle-f? and . {f?, On suppose que F ? {F? : (x, l)

?. P. Par-la-règle, [. C-r-,-c-s-?{v-w}};-f-,-c-r-,-c-s-?{w-v}}]-est-un-ltbitableau-pour, F. Donc, and F. ,

F. Donc and ?. P. {v-w}}-?-p-ou-f-,-c-r-,-c-s-?-{w-v}}, 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 )

. On-suppose-que-f?-;-x,-u)-?-f, 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. Annexe,

. F-i-,-c-ri,

, A r (C ri ) ? {1 r , c 1 , c 2, p.2

?. P. ?-f-?-et-f?-;-?-f-?-et-x-y-?-c-r?-.-alors-f-?-,-c-r?-;-f-?-,-c-r?, 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

. F-?-?-{t?-;-x,-u)},-c-r?-,-c-s?-?-p-et-f-?-?-{t?-;-},-c-r?, 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)

F. On-suppose-que-f???-;-x,-u)-?-f-?-.-comme-p-est-saturé and . ?-?{f?-;-x,-u)},-c-r?-,-c-s?-?-p-ou-f-?-?-{f?, s? ? P par la règle F?. Par la propriété 2 de la Propo

, Similaire à la condition 8

, Similaire à la condition 7

?. Soit-c-?-l-r-tel-que-x-c-?-c-r?-.-comme-p-est-saturé and F. ?-?-{f?-;-c,-u)},-c-r?-,-c-s?-?-p-ou-f-?-?-{t?, On suppose que T? ? ? : (x, u)

C. ?-f-k--f-k, ?. P. Rk, . On-a-donc-f-k+1, and . {t?, 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)

. Donc-f-k+1-,-c-rk+1-,-c-sk+1-=-f-k-?-{t?-;-}, C. {ab-x}, and . Sk-;-?-f-?-et-t?-;-?-f-?-.-14-;-},-c-r?-,-c-s?-?-p-ou-f-?-?-{f?-;-d,-u)},-c-r?-,-c-s?-?-p-par-la-règle-f-*-*, 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

C. On-suppose-que-t??-;-?-f-?-;-?-f-k--f-k and C. Rk, 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)

). Alors-f-k+1 and C. Rk,

. On-suppose-que-f??-;-?-f-?, 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

F. On-suppose-que-u-v-?-c-s?-et-u-w-?-c-s?, C. R?, C. {v-w}}-?-p-ou-f-?, and . R?, C s? ? {w v}} ? P par la règle . Alors, par la propriété 3 de la Proposition

F. On-suppose-que-u-v-?-c-s?-et-u-w-?-c-s?, C. R?, and . {u-w}}-?-p-ou-f-?-,-c-r?,

V. , E. )-un-c-tableau, and . Soit-c-?-v-un-tpn-réalisable, 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

S. , (. , and C. , 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

F. and F. , On note R = (K , ., s) la réalisation de C

A. Annexe,

, -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

. Dans-ce-cas-i-:-x-?-f-+, 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

. Dans-ce-cas-a-?-b-:-x-?-f-+, 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

F. Dans-ce-cas-a-?-b-:-x-?-f-?-;-tpn-f-+ and . ?{a, 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

. Dans-ce-cas-a-?-b-:-x-?-f-+-;-f-?-,-c-r-et-f-+-?{b, 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

. Dans-ce-cas-a-?-b-:-x-?-f-?, 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

F. Dans-ce-cas-a-?-b-:-x-?-f-+-et-x-y-?-c-r-;-tpn-f-+-\-{a-?-b-:-x}, \. {a-:-x},-c-r-et-f-+-?-{b-:-x}, and F. {a-?-b-:-x}, 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

. Dans-ce-cas-a-?-b-:-x-?-f-?-;-k-a-?-b, 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

. Dans-ce-cas-a-*-b-:-x-?-f-+, 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

F. Une-réalisation-du-nouveau-tpn-f-+-?-{a-:-c-i-,-b-:-c-j-}-\-{a-*-b-:-x} and . {c-i-c-j-x}},

F. Dans-ce-cas-a-*-b-:-x-?-f-?-et-yz-x-?-c-r-;-tpn-f-+, \. {a-:-y}, F. {a-*-b-:-x}, F. {b-:-z}, and \. {a-*-b-:-x}, 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

. Dans-ce-cas-a-?-*-b-:-x-?-f-+-et-xy-xy-?-c-r, 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'

F. Donc-r-est-une-réalisation-d'un-des-nouveaux-tpn-f-+-\-{a-?-b-:-x}, \. {a-:-y},-c-r-et-f-+-?-{b-:-xy}, and F. {a-?-b-:-x},

}. Dans-ce-cas-a-?-*-b-:-x-?-f-?-;-k-a-?-*-b-;-k-a-et-(x-?-r,-s)-k-b-;-tpn-f-+-?-{a-:-c-i, F. {b-:-xc-i-}-\-{a-?-*-b-:-x},-c-r-?-{xc-i-xc-i-}}, F. Tpn-f-+, and . {a, 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)

. 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

F. {?a-:-x}, C. Et-f-+-?-{??a-:-x}-\-{?a-:-x}, and F. ,

. 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 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

-. ??-;-?-f-.-comme-f-est-réalisable,-on-a-x-k-?-?-?,-ce-qui-veut-dire-que-x-k-?-et-x-k-?, 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

K. ?-a(f-),-?-n-;-on-définit-donc-le-modèle and . Est-une-réalisation-de-la-nouvelle-branche-f-?-{t-@-c-i, 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

. Alors-on-a-t-@-x-(?-?-*-?)-?-f-et-t-@-z-(x-*-y)-?-f-.-comme-f-est-réalisable,-on-a-x-k-?-?-*-?-et-z-k-x-*-y, 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

. Dans-le, 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-ou-f-@-x,

. Si-t-@-x-(?-*-?)-?-f and . Nom\a,

. Si-f-@-x-(?-?-*-?)-?-f and . Nom\a, F ) tel que c i = c j et F ? {T @ c i (?), F @ c j (?) T @ c j (x * c i )} ? P

. Si-f-@-x-(?-*-?-?)-?-f and . Nom\a,

F. Si-f-@-x-;-?-f-et-t-@-x-(y)-?-f and . {f-@-y-;-}-?-p,

. Si-t-@-x, T @ c i (y * z)} ? P pour toute substitution

. Si-f-@-x, T @ c i (y * z)} ? P pour toute substitution

. Si-t-@-x-;-?-f-et-t-@-y-;-}-?-p,

F. Si-f-@-x-;-?-f-et-t-@-y-;-?-f and . {f-@-x-;-}-?-p,

, 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 (?)})

L. ,

, Proposition B.4. Pour toute substitution ?

, Si F f est un SHS fini, alors ?(F ) est un SHS fini

F. Si, alors ?(F ) ? ?(F )

|. , La preuve est directe étant donné que |?(F )

F. Soit and . Tels-que-f-?-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

. Soit-p-une-propriété-de-consistance-?-close,

?. En-outre and . {t-@-x, } ? P , donc par saturation par la règle i+

}. {t-@-x, 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

.. Nom-e-?-{c-1,

?. En-outre and . {f-@-x, } ? P , donc par saturation par la règle i+

}. {f-@-x, 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

. F-?-t-@-x-(x-*-i)-?-p,

, 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

. Si-t-est-de-taille-1 and . {f?, {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)

R. -si, . Bbi, C. Ti-:-x-dans-t-sur-laquelle-la-règle-est-appliquée.-c'est-À-dire-que-t-=-t-a-?-f, . ?-t-b, ?. F. Ti-:-x et al.,

R. Si, . Bbi, C. Une-formule-t?-?-?-:-x-dans-t-sur-laquelle-la-règle-est-appliquée.-c'est-À-dire-que-t-=-t-a-?-f, and ?. ?-t-b-et-t?, 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 )

. Dans-le-cas-où-x-est and . Composé, ? ?) ? 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 )

R. Si, . Bbi, C. Une-formule-f?-?-?-:-x-dans-t-sur-laquelle-la-règle-est-appliquée.-c'est-À-dire-que-t-=-t-a-?-f, and ?. ?-t-b-et-f?, 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

C. F-?-{f?-:-x},

F. {f-@-x, ? ?(T b ). Comme ?(T ) est un tableau par (HR), ?(T ) l'est aussi par application de la règle F? à ?(T )

. Dans-le-cas-où-x-est and . Composé, ? ?) ? 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 (?)

F. {f-@-c, T @ c (d(x))} ? ?(T b ) ce qui correspond à nouveau à l'application de la règle F?

R. Si, . Bbi, C. Une-formule-t?-*-?-:-x-dans-t-sur-laquelle-la-règle-est-appliquée.-c'est-À-dire-que-t-=-t-a-?-f, and *. ?-t-b-et-t?, 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

. T-@-x, Comme ?(T ) est un tableau par (HR), ?(T ) l'est aussi par application de la règle T * * à ?(T )

. Dans-le-cas-où-x-est and . Composé, * ?) ? 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 )

R. Si, . Bbi, C. Une-formule-f?-*-?-:-x-dans-t-sur-laquelle-la-règle-est-appliquée.-c'est-À-dire-que-t-=-t-a-?-f, and . ?-t-b-et-f?-*-?-:-x-?-f-et-x-yz-?-c, 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

F. {f-@-z,

, 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)

. -f-:-x-?-f-.-alors-f-@-x-;-?-f-et-f-est-clos and . Ou-bien-f-@-y-;-?-f-et-t-@-y-;-?-f, 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

. T-)-est-clos and F. Soit, 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

. T-@-x-;-?)-?-f, 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

. F-@-x, 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

F. Dans-tous-les-cas, Comme ceci est vrai pour tout CSS, T est clos