Search results for "Proof"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
20	William Billingsley, Peter Robinson 0001	Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Intelligent book, MathsTiles, Isabelle
20	Roberto Maieli	Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic.	LPAR	2007	DBLP DOI BibTeX RDF
20	Stefan S. Dantchev, Barnaby Martin, Stefan Szeider	Parameterized Proof Complexity.	FOCS	2007	DBLP DOI BibTeX RDF
20	Vuong Xuan Tran, Hidekazu Tsuji	Proof for Multi-agent Communication of Semantic Web Information.	CIT	2007	DBLP DOI BibTeX RDF
20	Grigoris Antoniou, Antonis Bikakis, Nikos Dimaresis, Manolis Genetzakis, Giannis Georgalis, Guido Governatori, Efie Karouzaki, Nikolaos Kazepis, Dimitris Kosmadakis, Manolis Kritsotakis, Giannis Lilis, Antonis Papadogiannakis, Panagiotis Pediaditis, Constantinos Terzakis, Rena Theodosaki, Dimitris Zeginis	Proof Explanation for the Semantic Web Using Defeasible Logic.	KSEM	2007	DBLP DOI BibTeX RDF
20	Atsushi Iwasaki, David Kempe 0001, Yasumasa Saito, Mahyar Salek, Makoto Yokoo	False-Name-Proof Mechanisms for Hiring a Team.	WINE	2007	DBLP DOI BibTeX RDF
20	Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie	The MOBIUS Proof Carrying Code Infrastructure.	FMCO	2007	DBLP DOI BibTeX RDF
20	Georges Gonthier	The Four Colour Theorem: Engineering of a Formal Proof.	ASCM	2007	DBLP DOI BibTeX RDF
20	Gilles Dowek, Olivier Hermant	A Simple Proof That Super-Consistency Implies Cut Elimination.	RTA	2007	DBLP DOI BibTeX RDF
20	Farhad Mehta	Supporting Proof in a Reactive Development Environment.	SEFM	2007	DBLP DOI BibTeX RDF
20	Serge Autexier, Armin Fiedler, Thomas Neumann 0006, Marc Wagner 0001	Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
20	David Aspinall 0001, Christoph Lüth, Daniel Winterstein	A Framework for Interactive Proof.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
20	Amine Chaieb	Proof-Producing Program Analysis.	ICTAC	2006	DBLP DOI BibTeX RDF
20	Mads Dam	Decidability and proof systems for language-based noninterference relations.	POPL	2006	DBLP DOI BibTeX RDF	intransitive noninterference, information flow, language-based security, noninterference, multi-level security
20	Herman Geuvers, Iris Loeb	From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions.	MFCS	2006	DBLP DOI BibTeX RDF
20	Huabing Yang, Xingyuan Zhang, Yuanyuan Wang	A correctness proof of the SRP protocol.	IPDPS	2006	DBLP DOI BibTeX RDF
20	Serge Autexier, Dominik Dietrich	Synthesizing Proof Planning Methods and Omega-Ants Agents from Mathematical Knowledge.	MKM	2006	DBLP DOI BibTeX RDF
20	Michael Backes 0001, Markus Dürmuth	A Cryptographically Sound Dolev-Yao Style Security Proof of an Electronic Payment System.	CSFW	2005	DBLP DOI BibTeX RDF
20	Martin Hofmann 0001	Proof-Theoretic Approach to Description-Logic.	LICS	2005	DBLP DOI BibTeX RDF
20	Peter B. Andrews	Some Reflections on Proof Transformations.	Mechanizing Mathematical Reasoning	2005	DBLP DOI BibTeX RDF
20	Claudio Castellini, Alan Smaill	Proof Planning for First-Order Temporal Logic.	CADE	2005	DBLP DOI BibTeX RDF
20	Ulrich Kohlenbach	Proof Mining in Functional Analysis.	CiE	2005	DBLP DOI BibTeX RDF
20	Gilles Barthe, Tamara Rezk, Ando Saabas	Proof Obligations Preserving Compilation.	Formal Aspects in Security and Trust	2005	DBLP DOI BibTeX RDF
20	David Billington	The Proof Algorithms of Plausible Logic Form a Hierarchy.	Australian Conference on Artificial Intelligence	2005	DBLP DOI BibTeX RDF
20	David Aspinall 0001, Christoph Lüth, Burkhart Wolff	Assisted Proof Document Authoring.	MKM	2005	DBLP DOI BibTeX RDF
20	Michael Backes 0001, Birgit Pfitzmann	A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol.	IEEE J. Sel. Areas Commun.	2004	DBLP DOI BibTeX RDF
20	Richard Sommer, Gregory Nuckols	A Proof Environment for Teaching Mathematics.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	EPGY Theorem Proving Environment, computer-based learning, automated reasoning
20	Olivier Boite	Proof Reuse with Extended Inductive Types.	TPHOLs	2004	DBLP DOI BibTeX RDF
20	Olivier Fissore, Isabelle Gnaedig, Hélène Kirchner	A Proof of Weak Termination Providing the Right Way to Terminate.	ICTAC	2004	DBLP DOI BibTeX RDF
20	Nina Amla, Kenneth L. McMillan	A Hybrid of Counterexample-Based and Proof-Based Abstraction.	FMCAD	2004	DBLP DOI BibTeX RDF
20	J. B. Wells, Boris Yakobowski	Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis.	LOPSTR	2004	DBLP DOI BibTeX RDF
20	Takayuki Suyama, Makoto Yokoo	Strategy/False-name Proof Protocols for Combinatorial Multi-Attribute Procurement Auction.	AAMAS	2004	DBLP DOI BibTeX RDF
20	Claudio Sacerdoti Coen	Mathematical Libraries as Proof Assistant Environments.	MKM	2004	DBLP DOI BibTeX RDF
20	Alexander V. Lyaletski, Andrey Paskevich, Konstantin Verchinine	Theorem Proving and Proof Verification in the System SAD.	MKM	2004	DBLP DOI BibTeX RDF
20	Roberto Maieli	A new correctness criterion for multiplicative non-commutative proof nets.	Arch. Math. Log.	2003	DBLP DOI BibTeX RDF
20	Paul Beame, Russell Impagliazzo, Toniann Pitassi, Nathan Segerlind	Memoization and DPLL: Formula Caching Proof Systems.	CCC	2003	DBLP DOI BibTeX RDF
20	Hirotada Kobayashi, Keiji Matsumoto	Quantum Multi-prover Interactive Proof Systems with Limited Prior Entanglement.	ISAAC	2002	DBLP DOI BibTeX RDF
20	Alan Bundy	A Critique of Proof Planning.	Computational Logic: Logic Programming and Beyond	2002	DBLP DOI BibTeX RDF
20	Mitchell Wand, Galen B. Williamson	A Modular, Extensible Proof Method for Small-Step Flow Analyses.	ESOP	2002	DBLP DOI BibTeX RDF
20	Alexandre Miquel, Benjamin Werner	The Not So Simple Proof-Irrelevant Model of CC.	TYPES	2002	DBLP DOI BibTeX RDF
20	Dominique Cansell, Ganesh Gopalakrishnan, Michael D. Jones, Dominique Méry, Airy Weinzoepflen	Incremental Proof of the Producer/Consumer Property for the PCI Protocol.	ZB	2002	DBLP DOI BibTeX RDF
20	Matthias Baaz, Agata Ciabattoni	A Schütte-Tait Style Cut-Elimination Proof for First-Order Gödel Logic.	TABLEAUX	2002	DBLP DOI BibTeX RDF
20	Florina Piroi, Bruno Buchberger	Focus Windows: A New Technique for Proof Presentation.	AISC	2002	DBLP DOI BibTeX RDF
20	Thomas Marthedal Rasmussen	Automated Proof Support for Interval Logics.	LPAR	2001	DBLP DOI BibTeX RDF
20	Pavel Naumov, Mark-Oliver Stehr, José Meseguer 0001	The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability).	TPHOLs	2001	DBLP DOI BibTeX RDF
20	George C. Necula	A Scalable Architecture for Proof-Carrying Code.	FLOPS	2001	DBLP DOI BibTeX RDF
20	Robin Milner	Graphical Theories of Interactive Systems: Can a Proof Assistant Help?	TPHOLs	2000	DBLP DOI BibTeX RDF
20	Huimin Lin, Wang Yi 0001	A Proof System for Timed Automata.	FoSSaCS	2000	DBLP DOI BibTeX RDF
20	Danny Gutfreund, Michael Ben-Or	Increasing the Power of the Dealer in Non-interactive Zero-Knowledge Proof Systems.	ASIACRYPT	2000	DBLP DOI BibTeX RDF
20	Steve King 0001, Jonathan Hammond, Roderick Chapman, Andy Pryor	The Value of Verification: Positive Experience of Industrial Proof.	World Congress on Formal Methods	1999	DBLP DOI BibTeX RDF
20	James L. Caldwell	Classical Propositional Decidability via Nuprl Proof Extraction.	TPHOLs	1998	DBLP DOI BibTeX RDF
20	Jean-Christophe Filliâtre	Proof of Imperative Programs in Type Theory.	TYPES	1998	DBLP DOI BibTeX RDF
20	Bernhard K. Aichernig, Peter Gorm Larsen	A Proof Obligation Generator for VDM-SL.	FME	1997	DBLP DOI BibTeX RDF
20	Matthias Fuchs	Experiments in the Heuristic Use of Past Proof Experience.	CADE	1996	DBLP DOI BibTeX RDF
20	Catholijn M. Jonker	Proof-theory for Extensions of Logic Programming.	ELP	1996	DBLP DOI BibTeX RDF	Rule-based calculus, program completions, negations
20	S. Rajan, Natarajan Shankar, Mandayam K. Srivas	An Integration of Model Checking with Automated Proof Checking.	CAV	1995	DBLP DOI BibTeX RDF
20	Mads Dam	Compositional Proof Systems for Model Checking Infinite State Processes.	CONCUR	1995	DBLP DOI BibTeX RDF
20	Atsushi Fujioka, Tatsuaki Okamoto, Kazuo Ohta	Interactive Bi-Proof Systems and Undeniable Signature Schemes.	EUROCRYPT	1991	DBLP DOI BibTeX RDF
20	Charles Rackoff, Daniel R. Simon	Non-Interactive Zero-Knowledge Proof of Knowledge and Chosen Ciphertext Attack.	CRYPTO	1991	DBLP DOI BibTeX RDF
20	James H. Andrews	Proof-Theoretic Characterisations of Logic Programs.	MFCS	1989	DBLP DOI BibTeX RDF
20	Milind Gandhe, G. Venkatesh	Improving Prolog Performance by Inductive Proof Generalizations.	KBCS	1989	DBLP DOI BibTeX RDF
20	Natarajan Shankar	A mechanical proof of the Church-Rosser theorem.	J. ACM	1988	DBLP DOI BibTeX RDF
20	Baruch Awerbuch, Lefteris M. Kirousis, Evangelos Kranakis, Paul M. B. Vitányi	A Proof Technique for Register Automicity.	FSTTCS	1988	DBLP DOI BibTeX RDF
20	Jozef Hooman	A Compositional Proof Theory for Real-Time Distributed Message Passing.	PARLE (2)	1987	DBLP DOI BibTeX RDF
20	Alfredo De Santis, Silvio Micali, Giuseppe Persiano	Non-Interactive Zero-Knowledge Proof Systems.	CRYPTO	1987	DBLP DOI BibTeX RDF
20	Van Nguyen, David Gries, Susan S. Owicki	A Model and Temporal Proof System for Networks of Processes.	POPL	1985	DBLP DOI BibTeX RDF
20	Thomas W. Reps, Bowen Alpern	Interactive Proof Checking.	POPL	1984	DBLP DOI BibTeX RDF
20	Deepak Kapur, Balakrishnan Krishnamurthy	A Natural Proof System Based on rewriting Techniques.	CADE	1984	DBLP DOI BibTeX RDF
19	Yingying Jiang 0001, Feng Tian 0001, Hongan Wang, Xiaolong Zhang 0001, XuGang Wang, Guozhong Dai	Intelligent understanding of handwritten geometry theorem proving.	IUI	2010	DBLP DOI BibTeX RDF	geometry theorem proving, hand-drawn figures, hand-written proof scripts, structure based manipulation, recognition
19	Ross Tate, Michael Stepp, Sorin Lerner	Generating compiler optimizations from proofs.	POPL	2010	DBLP DOI BibTeX RDF	proof generalization, compiler optimization, explanation-based learning
19	Adam J. Lee, Kazuhiro Minami, Nikita Borisov	Confidentiality-preserving distributed proofs of conjunctive queries.	AsiaCCS	2009	DBLP DOI BibTeX RDF	distributed proof, pervasive computing, consistency
19	Eugene Goldberg	Boundary Points and Resolution.	SAT	2009	DBLP DOI BibTeX RDF	proof quality, resolution, SAT-solver, boundary points
19	Adam Chlipala	Parametric higher-order abstract syntax for mechanized semantics.	ICFP	2008	DBLP DOI BibTeX RDF	type-theoretic semantics, dependent types, compiler verification, interactive proof assistants
19	Nathan Segerlind	On the Relative Efficiency of Resolution-Like Proofs and Ordered Binary Decision Diagram Proofs.	CCC	2008	DBLP DOI BibTeX RDF	lower bounds, resolution, ordered binary decision diagrams, propositional proof complexity
19	Maria Paola Bonacina, Nachum Dershowitz	Abstract canonical inference.	ACM Trans. Comput. Log.	2007	DBLP DOI BibTeX RDF	proof orderings, fairness, redundancy, completeness, completion, Inference, saturation, canonicity
19	Mihály Csaba Markót, Tibor Csendes	A Reliable Area Reduction Technique for Solving Circle Packing Problems.	Computing	2006	DBLP DOI BibTeX RDF	Circle packing, area reduction, computer-assisted proof, interval arithmetic
19	Nuno Amálio, Susan Stepney, Fiona Polack	A Formal Template Language Enabling Metaproof.	FM	2006	DBLP DOI BibTeX RDF	formal development, patterns, templates, Z, proof
19	Stefano Guerrini, Patrizia Marzuoli	Commutative Locative Quantifiers for Multiplicative Linear Logic.	ICALP (2)	2006	DBLP DOI BibTeX RDF	Ludics, linear logic, proof nets
19	Xinyu Feng 0001, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni	Modular verification of assembly code with stack-based control abstractions.	PLDI	2006	DBLP DOI BibTeX RDF	assembly code verification, control abstractions, stack-based, modularity, proof-carrying code
19	Stephen A. Cook, Tsuyoshi Morioka	Quantified propositional calculus and a second-order theory for NC1.	Arch. Math. Log.	2005	DBLP DOI BibTeX RDF	Computational Complexity, Proof Complexity, Bounded Arithmetic
19	Fagen Li, Juntao Gao, Yupu Hu	ID-Based Threshold Unsigncryption Scheme from Pairings.	CISC	2005	DBLP DOI BibTeX RDF	(t,n) threshold, signcryption, Identity-based cryptography, zero knowledge proof
19	Markus Schneider 0001, Thomas Behr	Topological Relationships Between Complex Lines and Complex Regions.	ER	2005	DBLP DOI BibTeX RDF	topological constraint rule, proof-by-constraint-and-drawing, complex spatial data type, 9-intersection model, Topological predicate
19	Erik Rosenthal	Formal Versus Rigorous Mathematics: How to Get Your Papers Published.	TABLEAUX	2005	DBLP DOI BibTeX RDF	nature of proof, rigor, formal mathematics
19	Michael Soltys	Feasible Proofs of Matrix Properties with Csanky's Algorithm.	CSL	2005	DBLP DOI BibTeX RDF	Csanky’s algorithm, matrix algebra, Proof complexity
19	Alan Skelley	A Third-Order Bounded Arithmetic Theory for PSPACE.	CSL	2004	DBLP DOI BibTeX RDF	quantified propositional calculus, Bounded arithmetic, PSPACE, propositional proof complexity
19	Peter Dybjer, Qiao Haiyan, Makoto Takeyama	Verifying Haskell Programs by Combining Testing and Proving.	QSIC	2003	DBLP DOI BibTeX RDF	BDDs and Haskell, program verification, random testing, type theory, proof-assistants
19	Michael W. Whalen, Johann Schumann, Bernd Fischer 0002	Synthesizing Certified Code.	FME	2002	DBLP DOI BibTeX RDF	automatic program synthesis, code certification, program verification, automated theorem proving, proof-carrying code
19	Sorin Craciunescu	Proving the Equivalence of CLP Programs.	ICLP	2002	DBLP DOI BibTeX RDF	CLP(forall), logic programming, constraint, induction, proof system, reactive program, coinduction, CLP, Program equivalence
19	Ricardo Caferra, Nicolas Peltier, François Puitg	Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization.	Automated Deduction in Geometry	2000	DBLP DOI BibTeX RDF	Automated geometric reasoning, model (counter-example) building, proof structuring with diagrams, analogy, computer assisted learning
19	Frédéric Saubion, Igor Stéphan	On Implementation of Tree Synchronized Languages.	RTA	1999	DBLP DOI BibTeX RDF	Tree Synchronized Grammars, Prolog Implementation, Linear Logic, Proof Systems
19	Frank S. de Boer, Maurizio Gabbrielli, Elena Marchiori, Catuscia Palamidessi	Proving Concurrent Constraint Programs Correct.	ACM Trans. Program. Lang. Syst.	1997	DBLP DOI BibTeX RDF	strongest postcondition, constraint programming, dynamic scheduling, proof theory
19	David R. Lester, Sava Mintchev	Towards Machine-Checked Compiler Correctness for Higher-order Pure Functional Languages.	CSL	1994	DBLP DOI BibTeX RDF	Congruence Proof, Lambda Calculus, Denotational Semantics, Theorem Prover, Compiler Correctness
19	Robert Harper 0001, Furio Honsell, Gordon D. Plotkin	A Framework for Defining Logics.	J. ACM	1993	DBLP DOI BibTeX RDF	proof checking, interactive theorem proving, typed lambda calculus, formal systems
19	Zohar Manna, Richard J. Waldinger	Fundamentals of Deductive Program Synthesis.	IEEE Trans. Software Eng.	1992	DBLP DOI BibTeX RDF	deductive program synthesis, deductive-tableau system, theorem-proving framework, nonclausal resolution rule, induction rule, formal specification, artificial intelligence, specification, theorem proving, program testing, reasoning, inference mechanisms, proof
19	Gerald M. Karam, Raymond J. A. Buhr	Starvation and Critical Race Analyzers for Ada.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	race analyzers, critical race analysis tools, Ada designs, temporal analysis toolset, operational specification language, language interpreter, deadlock analyzer, starvation analyzer, set-theoretic model, deadlock analyzer, computation space, preprocessing phase, starvation tool, semiautomatic proof, nondeterministic rendezvous, human operator, design examples, Ada, software tools, programming, specification languages, system recovery, liveness, program interpreters
18	Zachary Tatlock, Sorin Lerner	Bringing extensibility to verified compilers.	PLDI	2010	DBLP DOI BibTeX RDF	compiler optimization, correctness, extensibility
18	Wojciech Buszkowski, Maciej Farulewski	Nonassociative Lambek Calculus with Additives and Context-Free Languages.	Languages: From Formal to Natural	2009	DBLP DOI BibTeX RDF
18	Eli Ben-Sasson, Prahladh Harsha, Oded Lachish, Arie Matsliah	Sound 3-Query PCPPs Are Long.	ICALP (1)	2008	DBLP DOI BibTeX RDF
18	Joxan Jaffar, Andrew E. Santosa, Razvan Voicu	A Coinduction Rule for Entailment of Recursively Defined Properties.	CP	2008	DBLP DOI BibTeX RDF
18	Paolo Tranquilli	A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic.	CSL	2008	DBLP DOI BibTeX RDF