Search results for "proof"

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