Démonstration automatique And NotC. Scharff
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 |
000618 | Dominique Larchey-Wendling [France] | Counter-model search in Gödel-Dummett logics |
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 |
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. | ![]() |