Démonstration automatique And NotDominique Larchey-Wendling
List of bibliographic references
Number of relevant bibliographic references: 26.| Ident. | Authors (with country if any) | Title |
|---|---|---|
| 000378 | Yannick Chevalier [France] ; Michaël Rusinowitch [France] | Hierarchical combination of intruder theories |
| 000385 | Pascal Fontaine [France] ; Jean-Yves Marion [France] ; Stephan Merz [France] ; Leonor Prensa Nieto [France] ; Alwen Tiu [France] | Expressiveness + automation + soundness : Towards combining SMT solvers and interactive proof assistants |
| 000398 | Maria Paola Bonacina [Italie] ; Silvio Ghilardi [Italie] ; Enrica Nicolini [Italie] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie, France] | Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures |
| 000458 | Tomasz Truderung [France, Pologne] | Regular protocols and attacks with regular knowledge |
| 000504 | Frédéric Blanqui [France] | Decidability of type-checking in the calculus of algebraic constructions with size annotations |
| 000507 | Véronique Cortier [France] ; Bogdan Warinschi [États-Unis] | Computationally sound, automated proofs for security protocols |
| 000578 | Francis Alexandre [France] ; Khaled Bsaïes [Tunisie] ; Moussa Demba [Tunisie] | Predicate synthesis from inductive proof attempt of faulty conjectures |
| 000664 | Siva Anantharaman [France] ; Paliath Narendran [États-Unis] ; Michael Rusinowitch [France] | Unification modulo ACUI plus homomorphisms/distributivity |
| 000672 | Harald Ganzinger [Allemagne] ; Jürgen Stuber [France] | Superposition with equivalence reasoning and delayed clause normal form transformation |
| 000681 | Eric Deplagne [France] ; Claude Kirchner [France] ; Hélène Kirchner [France] ; Quang Huy Nguyen [France] | Proof search and proof check for equational and inductive theorems |
| 000690 | Christophe Ringeissen [France] | Matching in a class of combined non-disjoint theories |
| 000719 | Jean-Raymond Abrial ; Dominique Cansell [France] | Click'n prove: Interactive proofs within Set Theory |
| 000762 | Abdessamad Imine [Tunisie] ; Yahya Slimani [Tunisie] ; Sorin Stratulat [France] | Using automated induction-based theorem provers for reasoning about concurrent systems |
| 000796 | L. Habert [France] ; J.-M. Notin [France] ; D. Galmiche [France] | LINK: A proof environment based on proof nets |
| 000813 | Eric Deplagne [France] ; Claude Kirchner [France] | Deduction versus computation: The case of induction |
| 000829 | Yannick Chevalier [France] ; Laurent Vigneron [France] | Automated unbounded verification of security protocols |
| 000874 | Alessandro Armando [Italie] ; Silvio Ranise [Italie, France] ; Michaël Rusinowitch [France] | Uniform derivation of decision procedures by superposition |
| 000A63 | P. De Groote [France] | The non-associative Lambek calculus with product in polynomial time |
| 000B30 | E. Monfroy [Pays-Bas] ; C. Ringeissen [France] | SoleX : A domain-independent scheme for constraint solver extension |
| 000B34 | E. Melis [Allemagne] ; J. Lieber [France] ; A. Napoli [France] | Reformulation in case-based reasoning |
| 000B62 | C. Lynch [États-Unis] ; C. Scharff [France] | Basic Completion with E-cycle Simplification |
| 000C31 | B. Chetali [États-Unis] ; B. Heyd [États-Unis] | Formal verification of concurrent programs in LP and in COQ : A comparative analysis |
| 000D02 | A. Napoli [France] ; J. Lieber [France] ; R. Curien [France] | Classification-based problem-solving in case-based reasoning |
| 000D62 | M. Rusinowitch [France] | Theorem-proving with resolution and superposition |
| 000D65 | M. Hermann ; C. Kirchner ; H. Kirchner | Implementations of term rewriting systems |
| 000D66 | N. Doggaz ; C. Kirchner | Completion for unification |
| This area was generated with Dilib version V0.6.33. |  |