Démonstration théorème And NotGanesh Gopalakrishnan
List of bibliographic references
Number of relevant bibliographic references: 38.| Ident. | Authors (with country if any) | Title |
|---|---|---|
| 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 |
| 000170 | Guillaume Burel [France] ; Claude Kirchner [France] | Regaining cut admissibility in deduction modulo using abstract completion |
| 000171 | Joris Rehm [France] | Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the event-B method |
| 000226 | Dominique Cansell [France] ; Dominique Méry [France] ; Cyril Proch [France] | System-on-chip design by proof-based refinement |
| 000397 | Silvio Ghilardi [Italie] ; Enrica Nicolini [Italie] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie, France] | Deciding extensions of the theory of arrays by integrating decision procedures and instantiation strategies |
| 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 |
| 000565 | G. Hanrot [France] ; M. Quercia ; P. Zimmermann | The middle product algorithm I. Speeding up the division and square root of power series |
| 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 |
| 000632 | David Deharbe [Brésil] ; Abdessamad Imine [France] ; Silvio Ranise [France] | Abstraction-driven verification of array programs |
| 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 |
| 000729 | Nicolas Biri [France] ; Didier Galmiche [France] | A separation logic for resource distribution |
| 000762 | Abdessamad Imine [Tunisie] ; Yahya Slimani [Tunisie] ; Sorin Stratulat [France] | Using automated induction-based theorem provers for reasoning about concurrent systems |
| 000775 | Didier Galmiche [France] ; Daniel Mery [France] ; David Pym [Royaume-Uni] | Resource tableaux |
| 000796 | L. Habert [France] ; J.-M. Notin [France] ; D. Galmiche [France] | LINK: A proof environment based on proof nets |
| 000808 | Germain Faure [France] ; Claude Kirchner [France] | Exceptions in the rewriting calculus |
| 000813 | Eric Deplagne [France] ; Claude Kirchner [France] | Deduction versus computation: The case of induction |
| 000822 | Silvio Ranise [France] | Combining generic and domain specific Reasoning by using contexts |
| 000841 | Jean-Raymond Abriall ; Dominique Cansell [France] ; Guy Laffitte [France] | "higher-order" mathematics in B |
| 000886 | D. Larchey-Wendling [France] ; D. Mery [France] ; Didier Galmiche [France] | STRIP : Structural sharing for efficient proof-search |
| 000899 | Christophe Ringeissen [France] | Matching with free function symbols : A simple extension of matching? |
| 000900 | Horatiu Cirstea [France] ; Claude Kirchner [France] ; Luigi Liquori [France] | Matching power |
| 000925 | Jürgen Stuber [France] | A model-based completeness proof of extended narrowing and Resolution |
| 000A05 | I. Cervesato [États-Unis] ; J. S. Hodas [États-Unis] ; F. Pfenning [États-Unis] | Efficient resource management for linear logic proof search |
| 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 |
| 000B37 | E. A. Cichon [France] ; E. T. Bittar [France] | Ordinal recursive bounds for Higman's theorem |
| 000B49 | C. Lynch [France] | Local simplification |
| 000B62 | C. Lynch [États-Unis] ; C. Scharff [France] | Basic Completion with E-cycle Simplification |
| 000C47 | L. Alonso [France] ; J. L. Remy [France] ; R. Schott [France] | A linear-time algorithm for the generation of trees |
| 000C73 | A. Bouhoula [France] | Using induction and rewriting to verify and complete parameterized specifications |
| 000C79 | L. Vigneron [France] ; A. Wasilewska [États-Unis] | Rough and modal algebras |
| 000D04 | N. Berregeb [France] ; A. Bouhoula [France] ; M. Rusinowtich [France] | Automated verification by induction with associative-commutative operators |
| 000D07 | B. Heyd [France] ; P. Gregut [France] | A modular coding of UNITY in COQ |
| 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 |
| 000D71 | YUDONG SUN [France] ; M.-C. Haton ; B. Devin | Integrating theorem proving and partial evaluation techniques for organic synthesis and teaching |
| This area was generated with Dilib version V0.6.33. |  |