|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 10695 occurrences of 4479 keywords
|
|
|
Results
Found 21465 publication records. Showing 21465 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
17 | Aarti Gupta, Malay K. Ganai, Pranav Ashar |
Lazy Constraints and SAT Heuristics for Proof-Based Abstraction. |
VLSI Design |
2005 |
DBLP DOI BibTeX RDF |
|
17 | Daniel Chonghwan Lee, Lih-feng Tsaur |
A proof that uncorrelated branch SNRs yield the lowest error rate for MRC receivers operating over Nakagami-m-fading channels. |
IEEE Trans. Wirel. Commun. |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Sara Negri, Jan von Plato, Thierry Coquand |
Proof-theoretical analysis of order relations. |
Arch. Math. Log. |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Einar Broch Johnsen, Christoph Lüth |
Theorem Reuse by Proof Term Transformation. |
TPHOLs |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Shmuel Katz, Awais Rashid |
From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems. |
RE |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Xianfeng Zhao, Yingxia Dai, Dengguo Feng |
A Generalized Method for Constructing and Proving Zero-Knowledge Watermark Proof Systems. |
IWDW |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Kentaro Kikuchi |
A Direct Proof of Strong Normalization for an Extended Herbelin?s Calculus. |
FLOPS |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Sandip Ray, J Strother Moore |
Proof Styles in Operational Semantics. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Lutz Straßburger, François Lamarche |
On Proof Nets for Multiplicative Linear Logic with Units. |
CSL |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Erica Melis, Andreas Meier 0002, Martin Pollet |
Adaptive Access to a Proof Planner. |
MKM |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Lev D. Beklemishev |
Proof-theoretic analysis by iterated reflection. |
Arch. Math. Log. |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Renate A. Schmidt, Ewa Orlowska, Ullrich Hustadt |
Two Proof Systems for Peirce Algebras. |
RelMiCS |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina |
A Formal Proof of Dickson's Lemma in ACL2. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Luís Cruz-Filipe, Bas Spitters |
Program Extraction from Large Proof Developments. |
TPHOLs |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Nicolas Oury |
Observational Equivalence and Program Extraction in the Coq Proof Assistant. |
TLCA |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Raphaël Montelatici |
Polarized Proof Nets with Cycles and Fixpoints Semantics. |
TLCA |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Domenico Cantone, Eugenio G. Omodeo, Jacob T. Schwartz, Pietro Ursino |
Notes from the Logbook of a Proof-Checker's Project. |
Verification: Theory and Practice |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Stefan Berghofer |
A Constructive Proof of Higman's Lemma in Isabelle. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Lujo Bauer, Michael A. Schneider, Edward W. Felten, Andrew W. Appel |
Access Control on the Web Using Proof-carrying Authorization. |
DISCEX (2) |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Michael Backes 0001, Birgit Pfitzmann |
A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol. |
FSTTCS |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Yuko Sakurai, Makoto Yokoo |
A false-name-proof double auction protocol for arbitrary evaluation values. |
AAMAS |
2003 |
DBLP DOI BibTeX RDF |
electronic commerce, mechanism design, double auction |
17 | Claudio Castellini, Alan Smaill |
Proof Planning for Feature Interactions: A Preliminary Report. |
LPAR |
2002 |
DBLP DOI BibTeX RDF |
|
17 | Micaela Mayero |
Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm). |
TPHOLs |
2002 |
DBLP DOI BibTeX RDF |
|
17 | Natarajan Shankar |
Little Engines of Proof. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
17 | Eugenio G. Omodeo, Jacob T. Schwartz |
A 'Theory' Mechanism for a Proof-Verifier Based on First-Order Set Theory. |
Computational Logic: Logic Programming and Beyond |
2002 |
DBLP DOI BibTeX RDF |
|
17 | Kenji Terada, Makoto Yokoo |
False-Name-Proof Multi-unit Auction Protocol Utilizing Greedy Allocation Based on Approximate Evaluation Values. |
PRIMA |
2002 |
DBLP DOI BibTeX RDF |
|
17 | Gilles Richard, Fatima Zohra Kettaf |
Proof Length as an Uncertainty Factor in ILP. |
Soft-Ware |
2002 |
DBLP DOI BibTeX RDF |
|
17 | Andreas Meier 0002, Volker Sorge, Simon Colton |
Employing Theory Formation to Guide Proof Planning. |
AISC |
2002 |
DBLP DOI BibTeX RDF |
|
17 | Milos Besta, Frank A. Stomp |
Mechanization of a Proof of String-Preprocessing in Boyer-Moore's Pattern Matching Algorithm. |
ICECCS |
2002 |
DBLP DOI BibTeX RDF |
|
17 | Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna |
A proof engine approach to solving combinational design automation problems. |
DAC |
2002 |
DBLP DOI BibTeX RDF |
|
17 | Guy Perrier |
Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions. |
LPAR |
2001 |
DBLP DOI BibTeX RDF |
|
17 | Zenon Sadowski |
On a P-optimal Proof System for the Set of All Satisfiable Boolean Formulas (SAT). |
MCU |
2001 |
DBLP DOI BibTeX RDF |
|
17 | Claudette Cayrol, Sylvie Doutre, Jérôme Mengin |
Dialectical Proof Theories for the Credulous Preferred Semantics of Argumentation Frameworks. |
ECSQARU |
2001 |
DBLP DOI BibTeX RDF |
|
17 | Naoki Matsumoto |
Simple proof of the Routh stability criterion based on order reduction of polynomials and principle of argument. |
ISCAS (1) |
2001 |
DBLP DOI BibTeX RDF |
|
17 | René Vestergaard, James Brotherston |
A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names. |
RTA |
2001 |
DBLP DOI BibTeX RDF |
|
17 | Erika Ábrahám-Mumm, Martin Steffen, Ulrich Hannemann |
Verification of Hybrid Systems: Formalization and Proof Rules in PVS. |
ICECCS |
2001 |
DBLP DOI BibTeX RDF |
deductive methods, machine-assisted verification, hybrid systems |
17 | Ewen Denney |
A Prototype Proof Translator from HOL to Coq. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
17 | Andrew W. Appel, Amy P. Felty |
A Semantic Model of Types and Machine Instructions for Proof-Carrying Code. |
POPL |
2000 |
DBLP DOI BibTeX RDF |
|
17 | Roberto Di Cosmo, Delia Kesner, Emmanuel Polonowski |
Proof Nets and Explicit Substitutions. |
FoSSaCS |
2000 |
DBLP DOI BibTeX RDF |
|
17 | Erica Melis, Andreas Meier 0002 |
Proof Planning with Multiple Strategies. |
Computational Logic |
2000 |
DBLP DOI BibTeX RDF |
|
17 | Mike Jackson 0003, Helen Lowe |
System Description: Interactive Proof Critics in XBarnacle. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
17 | Marino Miculan |
Formalizing a Lazy Substitution Proof System for µ-calculus in the Calculus of Inductive Constructions. |
ICALP |
1999 |
DBLP DOI BibTeX RDF |
|
17 | Frank S. de Boer, Willem P. de Roever, Ulrich Hannemann |
The Semantic Foundations of a Compositional Proof Method for Synchronously Communicating Processes. |
MFCS |
1999 |
DBLP DOI BibTeX RDF |
|
17 | Jochen Meßner |
On Optimal Algorithms and Optimal Proof Systems. |
STACS |
1999 |
DBLP DOI BibTeX RDF |
|
17 | Mireille Larnac, Janine Magnier, Vincent Chapurlat |
Simplification of Proof Procedures Based on the Path Condition Concepts. |
EUROCAST |
1999 |
DBLP DOI BibTeX RDF |
|
17 | Lev D. Beklemishev |
A proof-theoretic analysis of collection. |
Arch. Math. Log. |
1998 |
DBLP DOI BibTeX RDF |
Mathematics Subject Classification (1991): Primary: 03F30, Secondary: 03F05, 03D20 |
17 | Stuart Anderson, Konstantinos Tourlas |
Design for Proof: An Approach to the Design of Domain-Specific Languages. |
Formal Aspects Comput. |
1998 |
DBLP DOI BibTeX RDF |
Industrial critical systems, Domain-specific languages, Programmable controllers, Programming language design |
17 | Martin Wirsing, John N. Crossley, Hannes Peterreins |
Proof Normalization of Structured Algebraic Specifications Is Convergent. |
WADT |
1998 |
DBLP DOI BibTeX RDF |
|
17 | George C. Necula, Peter Lee 0001 |
Safe, Untrusted Agents Using Proof-Carrying Code. |
Mobile Agents and Security |
1998 |
DBLP DOI BibTeX RDF |
|
17 | Matthew Wilding |
A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
17 | Giorgio Levi, Paolo Volpe |
Derivation of Proof Methods by Abstract Interpretation. |
PLILP/ALP |
1998 |
DBLP DOI BibTeX RDF |
|
17 | Huimin Lin |
Complete Proof Systems for Observation Congruences in Finite-Control pi-Calculus. |
ICALP |
1998 |
DBLP DOI BibTeX RDF |
|
17 | Michael Alekhnovich, Samuel R. Buss, Shlomo Moran, Toniann Pitassi |
Minimum Propositional Proof Length is NP-Hard to Linearly Approximate. |
MFCS |
1998 |
DBLP DOI BibTeX RDF |
|
17 | Stephan Schmitt, Christoph Kreitz |
Deleting Redundancy in Proof Reconstruction. |
TABLEAUX |
1998 |
DBLP DOI BibTeX RDF |
|
17 | Jeremy E. Dawson, Rajeev Goré |
A Mechanised Proof System for Relation Algebra using Display Logic. |
JELIA |
1998 |
DBLP DOI BibTeX RDF |
|
17 | Julian Richardson |
Abstract: Proof Planning with Program Schemas. |
LOPSTR |
1998 |
DBLP DOI BibTeX RDF |
|
17 | Jamie Stark, Andrew Ireland |
Invariant Discovery via Failed Proof Attempts. |
LOPSTR |
1998 |
DBLP DOI BibTeX RDF |
|
17 | Uwe Egly, Stephan Schmitt |
Intuitionistic Proof Transformations and Their Application to Constructive Program Synthesis. |
AISC |
1998 |
DBLP DOI BibTeX RDF |
|
17 | Quintijn Puite, Harold Schellinx |
On the Jordan-Hölder decomposition of proof nets. |
Arch. Math. Log. |
1997 |
DBLP DOI BibTeX RDF |
|
17 | Martin Simons 0001 |
Proof Presentation for Isabelle. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
17 | Roberto Di Cosmo, Delia Kesner |
Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract). |
LICS |
1997 |
DBLP DOI BibTeX RDF |
|
17 | Devendra Kumar, S. Sitharama Iyengar |
A Semiformal Correctness Proof of a Network Broadcast Algorithm. |
COMPSAC |
1997 |
DBLP DOI BibTeX RDF |
|
17 | Andrei Voronkov |
Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
17 | Aravind K. Joshi, Seth Kulick |
Partial Proof Trees, Resource Sensitive Logics, and Syntactic Constraints. |
LACL |
1996 |
DBLP DOI BibTeX RDF |
|
17 | Manfred Kerber, Michael Kohlhase, Volker Sorge |
Integrating Computer Algebra with Proof Planning. |
DISCO |
1996 |
DBLP DOI BibTeX RDF |
|
17 | Bikash Chandra Ghosh, Vilas Wuwongse |
A Direct Proof Procedure for Definite Conceptual Graph Programs. |
ICCS |
1995 |
DBLP DOI BibTeX RDF |
|
17 | Yves Ledru |
Proof-Based Development of Specifications with KIDS/VDM. |
FME |
1994 |
DBLP DOI BibTeX RDF |
|
17 | Bradley L. Richards, Ina Kraan, Alan Smaill, Geraint A. Wiggins |
Mollusc: A General Proof-Development Shell for Sequent-Based Logics. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
17 | Joachim Posegga |
Compiling Proof Search in Semantic Tableaux. |
ISMIS |
1993 |
DBLP DOI BibTeX RDF |
|
17 | Toby Walsh |
General Purpose Proof Plans. |
DISCO |
1993 |
DBLP DOI BibTeX RDF |
|
17 | Seppo Keronen |
Natural Deduction Proof Theory for Logic Programming. |
ELP |
1992 |
DBLP DOI BibTeX RDF |
|
17 | Kastytis Gecas |
A Compositional Proof System for Distributed Programs. |
Baltic Computer Science |
1991 |
DBLP DOI BibTeX RDF |
|
17 | Li-Yan Yuan, Jia-Huai You, Cheng Hui Wang |
A Proof-Theoretic Framework for Nonmonotonic Reasoning and Logic Programming. |
ICCI |
1991 |
DBLP DOI BibTeX RDF |
|
17 | Donald Beaver, Joan Feigenbaum, Victor Shoup |
Hiding Instances in Zero-Knowledge Proof Systems (Extended Abstract). |
CRYPTO |
1990 |
DBLP DOI BibTeX RDF |
|
17 | Jozef Hooman, Jennifer Widom |
A Temporal-Logic Based Compositional Proof System for Real-Time Message Passing. |
PARLE (2) |
1989 |
DBLP DOI BibTeX RDF |
|
17 | Chyuan Samuel Hsieh, Elizabeth A. Unger |
Resource scheduling: specification and proof techniques. |
ACM Conference on Computer Science |
1988 |
DBLP DOI BibTeX RDF |
|
17 | Yukihide Takayama |
QPC: QJ-based Proof Compiler - Simple Examples and Analysis. |
ESOP |
1988 |
DBLP DOI BibTeX RDF |
|
17 | D. Duchier, Drew V. McDermott |
LOGICALC: An Environment for Interactive Proof Development. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
17 | Kim Guldstrand Larsen |
Proof System for Hennessy-Milner Logic with Recursion. |
CAAP |
1988 |
DBLP DOI BibTeX RDF |
|
17 | Alan D. Fekete, Nancy A. Lynch, Liuba Shrira |
A Modular Proof of Correctness for a Network Synchronizer (Research Summary). |
WDAG |
1987 |
DBLP DOI BibTeX RDF |
|
17 | Franz Oppacher, E. Suen |
Controlling Deduction with Proof Condensation and Heuristics. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
17 | Colin Sterling |
A Complete Modal Proof System for a Subset of SCCS. |
TAPSOFT, Vol.1 |
1985 |
DBLP DOI BibTeX RDF |
|
17 | Colin Stirling |
A Complete Compositional Model Proof System for a Subset of CCS. |
ICALP |
1985 |
DBLP DOI BibTeX RDF |
|
17 | Eugene W. Stark |
A Proof Technique for Rely/Guarantee Properties. |
FSTTCS |
1985 |
DBLP DOI BibTeX RDF |
|
17 | Zohar Manna, Amir Pnueli |
How to Cook a Temporal Proof System for Your Pet Language. |
POPL |
1983 |
DBLP DOI BibTeX RDF |
|
16 | Marc Daumas, Érik Martin-Dorel, Annick Truffert, Michel Ventou |
A Formal Theory of Cooperative TU-Games. |
MDAI |
2009 |
DBLP DOI BibTeX RDF |
automated proof checker, formalization, cooperative games |
16 | Jean-Baptiste Tristan, Xavier Leroy |
Verified validation of lazy code motion. |
PLDI |
2009 |
DBLP DOI BibTeX RDF |
lazy code motion, the coq proof assistant, redundancy elimination, translation validation, verified compilers |
16 | Vivek Nigam, Dale Miller 0001 |
Algorithmic specifications in linear logic with subexponentials. |
PPDP |
2009 |
DBLP DOI BibTeX RDF |
subexponentials, linear logic, proof search |
16 | Douglas Walton |
A dialogical theory of presumption. |
Artif. Intell. Law |
2008 |
DBLP DOI BibTeX RDF |
Burden of proof, Burden of persuasion, Shifting burden, Expert opinion evidence, Formal dialog systems, Evidence, Argumentation schemes |
16 | Luís Soares Barbosa, José Nuno Oliveira, Alexandra Silva 0001 |
Calculating Invariants as Coreflexive Bisimulations. |
AMAST |
2008 |
DBLP DOI BibTeX RDF |
coalgebraic reasoning, pointfree transform, proof obligations, program calculation |
16 | Andrew Gacek, Dale Miller 0001, Gopalan Nadathur |
Combining Generic Judgments with Recursive Definitions. |
LICS |
2008 |
DBLP DOI BibTeX RDF |
generic judgments, reasoning about operational semantics, higher-order abstract syntax, proof search |
16 | Clément Houtmann |
Axiom Directed Focusing. |
TYPES |
2008 |
DBLP DOI BibTeX RDF |
superdeduction, Proof theory, focusing, deduction modulo |
16 | José Nuno Oliveira |
Extended Static Checking by Calculation Using the Pointfree Transform. |
LerNet ALFA Summer School |
2008 |
DBLP DOI BibTeX RDF |
formal methods, Theoretical foundations, proof obligations, extended static checking |
16 | Gilles Brassard, Anne Broadbent, Esther Hänggi, André Allan Méthot, Stefan Wolf 0001 |
Classical, Quantum and Non-signalling Resources in Bipartite Games. |
ICQNM |
2008 |
DBLP DOI BibTeX RDF |
Nonlocality, Bell Theorems, Game Theory, Graph Theory, Interactive Proof Systems |
16 | Olaf Beyersdorff, Sebastian Müller 0003 |
A Tight Karp-Lipton Collapse Result in Bounded Arithmetic. |
CSL |
2008 |
DBLP DOI BibTeX RDF |
Karp-Lipton Theorem, Optimal Propositional Proof Systems, Extended Frege, Bounded Arithmetic, Advice |
16 | Andrew C. Doherty, Yeong-Cherng Liang, Ben Toner, Stephanie Wehner |
The Quantum Moment Problem and Bounds on Entangled Multi-prover Games. |
CCC |
2008 |
DBLP DOI BibTeX RDF |
quantum entanglement, nonlocal games, multi-prover interactive proof systems |
16 | Damiano Mazza, Michele Pagani |
The Separation Theorem for Differential Interaction Nets. |
LPAR |
2007 |
DBLP DOI BibTeX RDF |
Differential interaction nets, faithfulness, linear logic, observational equivalence, proof-nets |
16 | Nachum Dershowitz, Iddo Tzameret |
Complexity of Propositional Proofs Under a Promise. |
ICALP |
2007 |
DBLP DOI BibTeX RDF |
random 3CNF, promise problems, resolution, proof complexity |
16 | Luciano Gamberini, Giovanni Petrucci, Andrea Spoto, Anna Spagnolli |
Embedded Persuasive Strategies to Obtain Visitors' Data: Comparing Reward and Reciprocity in an Amateur, Knowledge-Based Website. |
PERSUASIVE |
2007 |
DBLP DOI BibTeX RDF |
social proof, persuasion, websites, reciprocity, personal information, reward |
16 | Arist Kojevnikov |
Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities. |
SAT |
2007 |
DBLP DOI BibTeX RDF |
integer programming, cutting planes, propositional proof complexity |
|
|