Programmation logique And NotD. Mery
List of bibliographic references
Number of relevant bibliographic references: 60.| Ident. | Authors (with country if any) | Title |
|---|---|---|
| 000017 | Hans Van Ditmarsch [France] ; Sujata Ghosh [Inde] ; Rineke Verbrugge [Pays-Bas] ; YANJING WANG [République populaire de Chine] | Hidden protocols: Modifying our expectations in an evolving world |
| 000140 | Khaled Gaaloul [Luxembourg (pays)] ; H. A. Proper [Luxembourg (pays)] ; Ehtesham Zahoor [France] ; François Charoy [France] ; Claude Godart [France] | A logical framework for reasoning about delegation policies in workflow management systems |
| 000335 | Florent Jacquemard [France] ; Michael Rusinowitch [France] ; Laurent Vigneron [France] | Tree automata with equality constraints modulo equational theories |
| 000337 | G. Bonfante [France] ; R. Kahle [Portugal] ; J.-Y. Marion [France] ; I. Oitavem [Portugal] | Towards an implicit characterization of NCk |
| 000353 | Véronique Cortier [France] ; Michaël Rusinowitch [France] ; Eugen Zalinescu [France] | Relating two standard notions of secrecy |
| 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 |
| 000431 | Florence Le Ber [France] ; Amedeo Napoli [France] | Relations, structures et objets : quelques variations |
| 000458 | Tomasz Truderung [France, Pologne] | Regular protocols and attacks with regular knowledge |
| 000468 | Carlos Areces [France] ; Daniel Gorin [Argentine] | Ordered resolution with selection for H(@) |
| 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 |
| 000504 | Frédéric Blanqui [France] | Decidability of type-checking in the calculus of algebraic constructions with size annotations |
| 000510 | Pascal Fontaine [France] ; Silvio Ranise [France] ; Calogero G. Zarba [France] | Combining lists with non-stably infinite theories |
| 000513 | Silvio Ranise [États-Unis] ; Christophe Ringeissen [États-Unis] ; Calogero G. Zarba [États-Unis] | Combining data structures with nonstably infinite theories using many-sorted logic |
| 000516 | Didier Galmiche [France] ; Daniel Mery [France] | Characterizing provability in BI's pointer logic through resource graphs |
| 000559 | Philippe De Groote [France] ; Bruno Guillaume [France] ; Sylvain Salvati [France] | Vector addition tree automata |
| 000578 | Francis Alexandre [France] ; Khaled Bsaïes [Tunisie] ; Moussa Demba [Tunisie] | Predicate synthesis from inductive proof attempt of faulty conjectures |
| 000600 | P. E. Moreau [France] ; O. Zendra | GC2: A generational conservative garbage collector for the ATerm library |
| 000618 | Dominique Larchey-Wendling [France] | Counter-model search in Gödel-Dummett logics |
| 000621 | Cesare Tinelli [États-Unis] ; Calogero G. Zarba [France] | Combining decision procedures for sorted theories |
| 000696 | Alberto Ciaffaglione [Italie] ; Luigi Liquori [France] ; Marino Miculan [Italie] | Imperative object-based calculi in co-inductive type theories |
| 000717 | D. Galmiche [France] ; J.-M. Notin [France] | Connection-based proof construction in non-commutative logic |
| 000719 | Jean-Raymond Abrial ; Dominique Cansell [France] | Click'n prove: Interactive proofs within Set Theory |
| 000746 | Alexander Bockmayr [France] ; Arnaud Courtois [France] | Modélisation de systèmes biologiques en programmation concurrente par contraintes hybrides |
| 000796 | L. Habert [France] ; J.-M. Notin [France] ; D. Galmiche [France] | LINK: A proof environment based on proof nets |
| 000881 | Horatiu Cirstea [France] | Specifying authentication protocols using rewriting and strategies |
| 000890 | Didier Galmiche [France] ; Daniel Mery [France] | Proof-search and countermodel generation in propositional BI logic |
| 000911 | Hubert Comon [France] ; Claude Kirchner [France] | Constraint solving on terms |
| 000954 | Proof-search in Type-theoretic Languages | |
| 000956 | D. Galmiche [France] | Workshop : Type-theoretic languages : Proof-search and semantics |
| 000961 | P. Narendran [États-Unis] ; M. Rusinowitch [France] | The theory of total unary RPO is decidable |
| 000963 | A. Felty [États-Unis] | The calculus of constructions as a framework for proof search with set variable instantiation |
| 000974 | D. Galmiche [France] ; D. J. Pym [Royaume-Uni] | Proof-search in type-theoretic languages : an introduction |
| 000976 | M. W. Bunder [Australie] | Proof finding algorithms for implicational logics |
| 000980 | G. Kucherov [France] ; M. Rusinowitch [France] | Patterns in words versus patterns in trees : A brief survey and new results |
| 000986 | E. Ritter [Royaume-Uni] ; D. Pym [Royaume-Uni] ; L. Wallen [Royaume-Uni] | On the intuitionistic force of classical search |
| 000990 | P. De Groote [France] | Linear higher-order matching is NP-complete |
| 000992 | J. Zhou [France] | Introduction to the constraint language NCL |
| 000999 | C. Ringeissen [France] ; E. Monfroy [Pays-Bas] | Generating propagation rules for finite domains : A mixed approach |
| 000A05 | I. Cervesato [États-Unis] ; J. S. Hodas [États-Unis] ; F. Pfenning [États-Unis] | Efficient resource management for linear logic proof search |
| 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 |
| 000A17 | L. Bachmair [États-Unis] ; I. V. Ramakrishnan [États-Unis] ; A. Tiwari [États-Unis] ; L. Vigneron [France] | Congruence closure modulo associativity and commutativity |
| 000A66 | D. Galmiche [France] ; D. Larchey-Wendling [France] | Structural sharing and efficient proof-search in propositional intuitionistic logic |
| 000A69 | P. De Groote [France] | On the strong normalisation of natural deduction with permutation-conversions |
| 000A71 | M. Hermann [France] ; L. Juban [France] ; P. G. Kolaitis [États-Unis] | On the complexity of counting the Hilbert basis of a linear Diophantine system |
| 000A82 | G. Dowek [France] ; T. Hardin [France] ; C. Kirchner [France] | Hol-λσ : An intentional first-order expression of higher-order logic |
| 000A99 | Y. Mokhtari [France] ; S. Merz [Allemagne] | Animating TLA specifications |
| 000B02 | H. Kirchner [France] ; P. D. Mosses [États-Unis] | Algebraic specifications, higher-order types, and set-theoretic models |
| 000B09 | P. De Groote [France] | A dynamic programming approach to categorical deduction |
| 000B49 | C. Lynch [France] | Local simplification |
| 000B93 | N. Lachiche [France] ; P. Marquis [France] | Classification par portée à partir de règles et d'exemples |
| 000C09 | A. Amaniss [France] ; M. Hermann ; D. Lugiez | Set operations for recurrent term schematizations |
| 000C15 | C. Retore [France] | Pomset logic : A non-commutative extension of classical linear logic |
| 000C19 | M. Hermann [France] ; P. G. Kolaitis [États-Unis] | On the complexity of unification and disunification in commutative idempotent semigroups |
| 000C25 | C. Kirchner [France] ; C. Ringeissen [France] | Higher-order equational unification via explicit substitutions |
| 000C54 | J. Jaray [France] ; A. Mahjoub [Tunisie] | Une méthode itérative de construction d'un modèle de système réactif |
| 000C67 | G. Perrier [France] | CPL : un modèle logique du calcul parallèle |
| 000D09 | M. Vittek [France] | A compiler for nondeterministic term rewriting systems |
| 000D46 | D. Galmiche [France] ; H. Kirchner [France] | Les langages fonctionnels et logiques |
| 000D65 | M. Hermann ; C. Kirchner ; H. Kirchner | Implementations of term rewriting systems |
| This area was generated with Dilib version V0.6.33. |  |