Search results for "proof"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
57	Eric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen 0002	Proof Search and Proof Check for Equational and Inductive Theorems.	CADE	2003	DBLP DOI BibTeX RDF	proof terms, computation, induction, automated theorem proving, deduction, rewrite rules, proof assistant
54	Kun Peng, Feng Bao 0001	Batch ZK Proof and Verification of OR Logic.	Inscrypt	2008	DBLP DOI BibTeX RDF	Batch proof and verification, knowledge statements linked with OR logic
53	Jean-Marc Andreoli	Focussing Proof-Net Construction as a Middleware Paradigm.	CADE	2002	DBLP DOI BibTeX RDF	Proof construction, Focussing, Middleware, Transactions, Proof search, Proof-nets
50	Steve King 0001, Jonathan Hammond, Roderick Chapman, Andy Pryor	Is Proof More Cost-Effective Than Testing?	IEEE Trans. Software Eng.	2000	DBLP DOI BibTeX RDF	specification proof, code proof, proof vs. testing, formal specification, Safety-critical software, industrial case study, SPARK
49	Martin Nordio, Peter Müller 0001, Bertrand Meyer 0001	Proof-Transforming Compilation of Eiffel Programs.	TOOLS (46)	2008	DBLP DOI BibTeX RDF	proof-transforming compiler, CIL, Software verification, Proof-Carrying Code, Eiffel, program proofs
48	Stefan Hetzl, Alexander Leitsch	Proof Transformations and Structural Invariance.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
47	Andrew Ireland, Mike Jackson 0003, Gordon Reid	Interactive Proof Critics.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Proof patching, Inductive proof, User interfaces, Theorem proving, Proof planning
46	HongDa Li 0001, Bao Li 0001	Existence of 3-round zero-knowledge proof systems for NP.	Sci. China Ser. F Inf. Sci.	2008	DBLP DOI BibTeX RDF	non-black-box simulation, DDH assumption, zero-knowledge proof, interactive proof
46	Dinghao Wu, Andrew W. Appel, Aaron Stump	Foundational proof checkers with small witnesses.	PPDP	2003	DBLP DOI BibTeX RDF	proof checker, proof-carrying code
45	David Aspinall 0001	Proof General: A Generic Tool for Proof Development.	TACAS	2000	DBLP DOI BibTeX RDF
45	Taiki Todo, Atsushi Iwasaki, Makoto Yokoo, Yuko Sakurai	Characterizing false-name-proof allocation rules in combinatorial auctions.	AAMAS (1)	2009	DBLP BibTeX RDF	false-name-proof, mechanism design, combinatorial auctions
45	Andrew Ireland, Jamie Stark	Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis.	Autom. Softw. Eng.	2006	DBLP DOI BibTeX RDF	partial order planning, deductive synthesis, program synthesis, proof planning
44	Boaz Barak, Oded Goldreich 0001	Universal Arguments and their Applications.	CCC	2002	DBLP DOI BibTeX RDF	Probabilistic proof systems, computationally-sound proof systems, zero-knowledge proof systems, probabilistic checkable proofs (PCP), collision-free hashing, witness indistinguishable proof systems, error-correcting codes, proofs of knowledge
44	Sándor Jenei, Franco Montagna	Rényi-Ulam Game Semantics for Product Logic and for the Logic of Cancellative Hoops.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
43	Didier Galmiche, J.-M. Notin	Proof-search and proof nets in Mixed Linear Logic.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
43	Natarajan Shankar	Using Proof Theory to Optimize Proof Search.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
43	Yasuyuki Tsukada	Interactive and Probabilistic Proof of Mobile Code Safety.	Autom. Softw. Eng.	2005	DBLP DOI BibTeX RDF	software verification, proof-carrying code, interactive proof system
43	Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni	A Syntactic Approach to Foundational Proof-Carrying Code.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	foundational proof-carrying code, syntactic soundness proof, typed assembly language
42	Kazuki Yoshizoe	A New Proof-Number Calculation Technique for Proof-Number Search.	Computers and Games	2008	DBLP DOI BibTeX RDF
42	L. Habert, J.-M. Notin, Didier Galmiche	LINK: A Proof Environment Based on Proof Nets.	TABLEAUX	2002	DBLP DOI BibTeX RDF
42	Karen Zee, Viktor Kuncak, Martin C. Rinard	An integrated proof language for imperative programs.	PLDI	2009	DBLP DOI BibTeX RDF	verification, theorem prover, proof system
42	Chih-Chung Lin, Yuan-Cheng Lai, J. D. Tygar, Chuan-Kai Yang, Chi-Lung Chiang	Coexistence Proof Using Chain of Timestamps for Multiple RFID Tags.	APWeb/WAIM Workshops	2007	DBLP DOI BibTeX RDF	coexistence proof, RFID, computer security, cryptographic protocol, timestamp, race condition
42	Ulrich Berger 0001	Program Extraction from Gentzen's Proof of Transfinite Induction up to epsilon0.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF
42	Kosta Dosen, Zoran Petric	Coherent Bicartesian and Sesquicartesian Categories.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF	categorial proof theory, conjunction and disjunction, decidability of equality of deductions Mathematics Subject Classification (2000): 18A30, 18A15, 03G30, 03F05
41	Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, Jan Johannsen	Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems.	FOCS	1998	DBLP DOI BibTeX RDF	Cutting Planes proof, tree-like proof, regular resolution, Davis-Putnam resolution, monotone real circuit, real communication complexity, lower bounds, resolution, propositional proof complexity
41	Irit Dinur, Omer Reingold	Assignment Testers: Towards a Combinatorial Proof of the PCP-Theorem.	FOCS	2004	DBLP DOI BibTeX RDF
41	Hisashi Hayashi	Knowledge Assimilation and Proof Restoration Through the Addition of Goals.	AIMSA	1998	DBLP DOI BibTeX RDF
41	Isabelle Gnaedig, Hélène Kirchner	Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
40	Ando Saabas, Tarmo Uustalu	Proof optimization for partial redundancy elimination.	PEPM	2008	DBLP DOI BibTeX RDF	program proof transformation, soundness and improvement of dataflow analyses and optimizations, type systems, proof-carrying code, partial redundancy elimination
40	Peter Müller 0001, Martin Nordio	Proof-transforming compilation of programs with abrupt termination.	SAVCBS	2007	DBLP DOI BibTeX RDF	proof-transforming compiler, proof-carrying code, trusted components
40	Stefan S. Dantchev	Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems.	STOC	2007	DBLP DOI BibTeX RDF	Lovász-Schrijver proof system, complexity gap theorems, lift and project methods, lower bounds, propositional proof complexity
39	Christian Urban, Bozhi Zhu	Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof.	RTA	2008	DBLP DOI BibTeX RDF
39	Lew Gordeev	Proof Theory and Post-turing Analysis.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF
39	Matthias Baaz, Christian G. Fermüller	A Note on the Proof-Theoretic Strength of a Single Application of the Schema of Identity.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF
38	Dale Miller 0001, Alexis Saurin	From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic.	CSL	2007	DBLP DOI BibTeX RDF
38	Jochen Meßner, Jacobo Torán	Optimal Proof Systems for Propositional Logic and Complete Sets.	STACS	1998	DBLP DOI BibTeX RDF
38	Yonatan Aumann, Uriel Feige	On Message Proof Systems with Known Space Verifiers.	CRYPTO	1993	DBLP DOI BibTeX RDF
37	Tobias Gedell, Reiner Hähnle	Verification by Parallelization of Parametric Code.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
37	Alexis Saurin	Towards Ludics Programming: Interactive Proof Search.	ICLP	2008	DBLP DOI BibTeX RDF	Ludics, Proof Normalization, Interaction, Logic Programming, Game Semantics, Proof Search
37	Andrew W. Appel, Neophytos G. Michael, Aaron Stump, Roberto Virga	A Trustworthy Proof Checker.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	proof checker, proof-carrying code
37	Yves Bertot	The CtCoq System: Design and Architecture.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Interactive proof development, CtCoq, Proof by pointing, Proof maintenance, Graphical user interfaces
36	Daniel Wasserrab, Denis Lohner, Gregor Snelting	On PDG-based noninterference and its modular proof.	PLAS	2009	DBLP DOI BibTeX RDF	modularity, program slicing, noninterference, correctness proof, program dependence graph
36	Marc Bezem, Dimitri Hendriks	On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Coherent logic, Proof objects, Hessenberg’s theorem, Automated theorem proving
36	Jamie Stark, Andrew Ireland	Towards Automatic Imperative Program Synthesis Through Proof Planning.	ASE	1999	DBLP DOI BibTeX RDF	Imperative Program Synthesis, Proof planning
36	Reinhard Kahle	Towards a Proof-Theoretic Semantics of Equalities.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
36	Wilfrid Hodges	A Strongly Differing Opinion on Proof-Theoretic Semantics?	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
36	Thomas Piecha, Peter Schroeder-Heister	Advances in Proof-Theoretic Semantics: Introduction.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
36	Thomas Piecha	Completeness in Proof-Theoretic Semantics.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
36	Warren D. Goldfarb	On Dummett's "Proof-Theoretic Justifications of Logical Laws".	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
36	Yoshihiro Maruyama	Categorical Harmony and Paradoxes in Proof-Theoretic Semantics.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
36	Lars Hallnäs	On the Proof-Theoretic Foundations of Set Theory.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
36	Peter Schroeder-Heister	Open Problems in Proof-Theoretic Semantics.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
36	Roy Dyckhoff	Some Remarks on Proof-Theoretic Semantics.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
36	John N. Crossley	What Is a Proof?	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
36	Mitsuhiro Okada, Ryo Takemura	Remarks on Semantic Completeness for Proof-Terms with Laird's Dual Affine/Intuitionistic lambda -Calculus.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
36	Sachio Hirokawa, Daisuke Nagano	Long Normal Form Proof Search and Counter-Model Generation.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
36	Nikos Mylonakis	Proof assistance for refinement in type theory.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
36	David J. Pym	Notes Towards a Semantics for Proof-search.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
36	Uwe Egly, Stephan Schmitt	Intuitionistic Proof Transformations: Complexity and Applications.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
36	Didier Galmiche, Bruno Martin	Proof nets Construction and Automated Deduction in Non-Commutative Linear Logic.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
36	Juan Bicarregui, Brian Matthews	The Specification and Proof of an EXPRESS to SQL "Compiler".	Proof in VDM	1998	DBLP DOI BibTeX RDF
36	Sten Agerholm, Jacob Frost	Supporting Proof in VDM-SL using Isabelle.	Proof in VDM	1998	DBLP DOI BibTeX RDF
36	John S. Fitzgerald, Cliff B. Jones	Proof in the Analysis of a Model of a Tracking System.	Proof in VDM	1998	DBLP DOI BibTeX RDF
36	Stefan Hougardy	Proof Checking and Non-approximability.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
36	Pavel Pudlák, Jirí Sgall	Algebraic models of computation and interpolation for algebraic proof systems.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
36	Chris Pollett	A propositional proof system for Ri2.	Proof Complexity and Feasible Arithmetics	1996	DBLP DOI BibTeX RDF
36	Henning Christiansen 0001	On Proof Predicates in Logic Programming.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
36	Roy Dyckhoff, Natarajan Shankar	Proof Search (Tutorial).	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
36	Sophie Coudert, Gilles Bernot, Pascale Le Gall	Hierarchical Heterogeneous Specifications.	WADT	1998	DBLP DOI BibTeX RDF	structured specification, heterogeneous proof, formal specification, modularity, algebraic specification, proof theory, logical framework, inference system, heterogeneous specification
35	Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier 0002, Claus-Peter Wirth	A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity.	MKM	2005	DBLP DOI BibTeX RDF
35	Phan Minh Dung, Paolo Mancarella, Francesca Toni	Argumentation-Based Proof Procedures for Credulous and Sceptical Non-monotonic Reasoning.	Computational Logic: Logic Programming and Beyond	2002	DBLP DOI BibTeX RDF
35	Martin Müller 0003	Proof-Set Search.	Computers and Games	2002	DBLP DOI BibTeX RDF
35	Johannes Köbler, Jochen Messner	Is the Standard Proof System for SAT P-Optimal?	FSTTCS	2000	DBLP DOI BibTeX RDF
35	Thierry Coquand, Henrik Persson	A Proof-Theoretical Investigation of Zantema's Problem.	CSL	1997	DBLP DOI BibTeX RDF
34	Jesse Alt, Sergei N. Artëmov	Reflective lambda-Calculus.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF
34	Marcelo Glusman, Shmuel Katz	A Mechanized Proof Environment for the Convenient Computations Proof Method.	Formal Methods Syst. Des.	2003	DBLP DOI BibTeX RDF	convenient computations, proof environment, deductive theorem proving, formal verification, PVS
34	Ruy J. G. B. de Queiroz	On Reduction Rules, Meaning-as-use, and Proof-theoretic Semantics.	Stud Logica	2008	DBLP DOI BibTeX RDF	reduction rules, proof-terms, proof-theoretic semantics, game-theoretic semantics, dialogue semantics, natural deduction
34	Søren Riis	On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity.	LICS	2008	DBLP DOI BibTeX RDF	Algebraic proof complexity, predicate logic, Propositional proof complexity
34	Kun Peng, Colin Boyd, Ed Dawson	Batch zero-knowledge proof and verification and its applications.	ACM Trans. Inf. Syst. Secur.	2007	DBLP DOI BibTeX RDF	Batch proof and verification of reencryption, batch proof and verification of decryption, mix network
34	Adam Chlipala	Modular development of certified program verifiers with a proof assistant.	ICFP	2006	DBLP DOI BibTeX RDF	programming with dependent types, proof-carrying code, interactive proof assistants
34	Willem C. Mallon, Jan Tijmen Udding	Using Metrics for Proof Rules for Recursively Defined Delay-insensitive Specifications.	ASYNC	1997	DBLP DOI BibTeX RDF	delay-insensitive specifications, recursive definition, linear proofs, intuitive induction rule, algebraic specification, algebraic specifications, theorem provers, correctness proofs, proof rules, proof rule
34	Maria Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, Toniann Pitassi	Non-Automatizability of Bounded-Depth Frege Proofs.	CCC	1999	DBLP DOI BibTeX RDF	Frege proof systems, automatizability of proof systems, interpolation, proof complexity
33	Allen Van Gelder	Independently Checkable Proofs from Decision Procedures: Issues and Progress.	LPAR	2005	DBLP DOI BibTeX RDF
33	Pinyan Lu, Xiaorui Sun, Yajun Wang 0001, Zeyuan Allen Zhu	Asymptotically optimal strategy-proof mechanisms for two-facility games.	EC	2010	DBLP DOI BibTeX RDF	strategy-proof, game theory, algorithmic mechanism design, social choice
33	Paul Beame, Trinh Huynh, Toniann Pitassi	Hardness amplification in proof complexity.	STOC	2010	DBLP DOI BibTeX RDF	communication complexity, proof complexity
33	Xinyu Feng 0001, Zhaozhong Ni, Zhong Shao, Yu Guo	An open framework for foundational proof-carrying code.	TLDI	2007	DBLP DOI BibTeX RDF	foundational proof-carrying code, open framework, interoperability, modularity, program verification
33	Bertrand Bellenot, Rene Brun, Gerardo Ganis, Jan Iwaszkiewicz, Guenter Kickinger, Andreas J. Peters, Fons Rademakers, Maarten Ballintijn, C. Loizides, C. Reed, Philippe Canal, Derek Feichtinger	PROOF - The Parallel ROOT Facility.	HPDC	2006	DBLP DOI BibTeX RDF	parallel ROOT facility, interactive distributed data set analysis, I/O utilization, CPU utilization, statistical tool, data access optimization, user session scheduling, user interface, grid computing, distributed storage, PROOF, visualization tool, heterogeneous clusters, multi-tier architecture
33	Dale Miller 0001, Alwen Tiu	A proof theory for generic judgments.	ACM Trans. Comput. Log.	2005	DBLP DOI BibTeX RDF	?-tree syntax, ?-quantifier, generic judgments, reasoning about operational semantics, higher-order abstract syntax, Proof search
33	Jürgen Zimmer, Erica Melis	Constraint Solving for Proof Planning.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	constraint satisfaction, automated reasoning, proof plans
33	Pierre Courtieu	Proving Self-Stabilization with a Proof Assistant.	IPDPS	2002	DBLP DOI BibTeX RDF	rewriting system on words, Self-stabilization, proof assistant
33	Naijun Zhan	Another formal proof for Deadline Driven Scheduler.	RTCSA	2000	DBLP DOI BibTeX RDF	Deadline Driven Scheduler, DDS correctness, random preemption, induction rules, induction propositions, intuitive facts, scheduling, real-time systems, theorem proving, process algebra, duration calculus, formal proof, DC
33	John Watrous	PSPACE Has Constant-Round Quantum Interactive Proof Systems.	FOCS	1999	DBLP DOI BibTeX RDF	quantum computation, interactive proof systems
33	Roberto Di Cosmo, Stefano Guerrini	Strong Normalization of Proof Nets Modulo Structural Congruences.	RTA	1999	DBLP DOI BibTeX RDF	Linear Logic, Proof Nets, Strong Normalization
33	Gleifer V. Alves, Anjolina Grisi de Oliveira, Ruy J. G. B. de Queiroz	Transformations via Geometric Perspective Techniques Augmented with Cycles Normalization.	WoLLIC	2009	DBLP DOI BibTeX RDF	proof-graphs, multiple conclusion, normalization, cycles, proof theory
33	Idit Keidar, Roger Khazan, Nancy A. Lynch, Alexander A. Shvartsman	An inheritance-based technique for building simulation proofs incrementally.	ACM Trans. Softw. Eng. Methodol.	2002	DBLP DOI BibTeX RDF	Inheritance by specialization and subclassing for extension, incremental proof techniques, proof reuse, simulation proofs, refinements
33	Venkatesan Guruswami, Daniel Lewin 0001, Madhu Sudan 0001, Luca Trevisan	A Tight Characterization of NP with 3 Query PCPs.	FOCS	1998	DBLP DOI BibTeX RDF	Probabilistically Checkable Proofs (PCP), Proof composition, Two-prover one-round proof systems, Adaptive and non-adaptive verifiers, Completeness and soundness, Complexity Theory, Query complexity
32	Thomas C. Hales	Formalizing the Proof of the Kepler Conjecture.	TPHOLs	2004	DBLP DOI BibTeX RDF
32	Atsushi Ohori	Register Allocation by Proof Transformation.	ESOP	2003	DBLP DOI BibTeX RDF
32	Freek Wiedijk	Formal Proof Sketches.	TYPES	2003	DBLP DOI BibTeX RDF
32	Robert R. Schneck, George C. Necula	A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code.	CADE	2002	DBLP DOI BibTeX RDF