Théorie preuve And NotSilvio Ghilardi
List of bibliographic references
Number of relevant bibliographic references: 30.| Ident. | Authors (with country if any) | Title |
|---|---|---|
| 000081 | Didier Galmiche [France] ; Daniel Mery [France] | A Connection-based Characterization of Bi-intuitionistic Validity |
| 000122 | Didier Galmiche [France] ; Yakoub Salhi [France] | Sequent calculi and decidability for intuitionistic hybrid logic |
| 000136 | Olfa Mosbahi [Allemagne] ; Mohamed Khalgui [Allemagne] | Combining formal methods for the development of reactive systems : DEVELOPMENT OF EMBEDDED SYSTEMS: MODELLING, VERIFICATION, SCHEDULING, IMPLEMENTATION AND RECONFIGURATION |
| 000171 | Joris Rehm [France] | Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the event-B method |
| 000260 | BOULBABA BEN AMMAR [France, Tunisie] ; MOHAMED TAHAR BHIRI [Tunisie] ; Jeanine Souquieres [France] | Modélisation événementielle pour la construction de diagrammes de classes |
| 000342 | Olivier Chevassut [États-Unis] ; Pierre-Alain Fouque [France] ; Pierrick Gaudry [France] ; David Pointcheval [France] | The Twist-AUgmented Technique for Key Exchange |
| 000375 | Nazim Benaïsa [France] ; Dominique Cansell [France] ; Dominique Méry [France] | Integration of security policy into system modeling |
| 000473 | Alessandro Armando [Italie] ; Maria Paola Bonacina [Italie] ; Silvio Ranise [France] ; Stephan Schulz [Italie] | On a rewriting approach to satisfiability procedures : Extension, combination of theories and an experimental appraisal |
| 000476 | Francois Lamarche [France] ; Lutz Strassburger [Allemagne] | Naming proofs in classical propositional logic |
| 000500 | Marco Bozzano [Italie] ; Roberto Bruttomesso [Italie] ; Alessandro Cimatti [Italie] ; Tommi Junttila [Finlande] ; Silvio Ranise [France] ; Peter Van Rossum [Pays-Bas] ; Roberto Sebastiani [Italie] | Efficient satisfiability modulo theories via delayed theory combination |
| 000632 | David Deharbe [Brésil] ; Abdessamad Imine [France] ; Silvio Ranise [France] | Abstraction-driven verification of array programs |
| 000642 | Damien Stehle [France] ; Paul Zimmermann [France] | A binary recursive Gcd algorithm |
| 000693 | Lutz Strassburger [France] | MELL in the calculus of structures |
| 000700 | Dominique Cansell [France] ; Dominique Méry [France] | Foundations of the B method |
| 000719 | Jean-Raymond Abrial ; Dominique Cansell [France] | Click'n prove: Interactive proofs within Set Theory |
| 000732 | Alessandro Armando [Italie] ; Silvio Ranise [Italie, France] ; Michaël Rusinowitch [France] | A rewriting approach to satisfiability procedures |
| 000786 | Philippe De Groote [France] | On the strong normalisation of intuitionistic natural deduction with permutation-conversions |
| 000813 | Eric Deplagne [France] ; Claude Kirchner [France] | Deduction versus computation: The case of induction |
| 000886 | D. Larchey-Wendling [France] ; D. Mery [France] ; Didier Galmiche [France] | STRIP : Structural sharing for efficient proof-search |
| 000890 | Didier Galmiche [France] ; Daniel Mery [France] | Proof-search and countermodel generation in propositional BI logic |
| 000901 | Guy Perrier [France] | Intuitionistic multiplicative proof nets as models of directed acyclic graph descriptions |
| 000954 | Proof-search in Type-theoretic Languages | |
| 000969 | A. Bouhoula [États-Unis, France] ; J.-P. Jouannaud [France] ; J. Meseguer [États-Unis] | Specification and proof in membership equational logic |
| 000970 | J. L. Caldwell [États-Unis] ; I. P. Gent [Royaume-Uni] ; J. Underwood [Royaume-Uni] | Search algorithms in type theory |
| 000975 | Philippe De Groote [France] | Proof-search in implicative linear logic as a matching problem |
| 000A14 | G. Nadathur [États-Unis] | Correspondences between classical, intuitionistic and uniform provability |
| 000A16 | D. Galmiche [France] | Connection methods in linear logic and proof nets construction |
| 000C78 | N. Berregeb [France] ; A. Bouhoula [France] ; M. Rusinowitch [France] | SPIKE-AC : A system for proofs by induction in associative-commutative theories |
| 000D01 | C. Hintermeier [France] ; H. Kirchner [France] ; P. D. Mosses [Danemark] | Combining algebraic and set-theoretic specifications |
| 000D42 | D. Galmiche [France] ; G. Perrier | On proof normalization in linear logic |
| This area was generated with Dilib version V0.6.33. |  |