Search results for "proof"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
32	Matthias Baaz	Proof Analysis by Resolution.	TABLEAUX	2002	DBLP DOI BibTeX RDF
32	Shin-ya Katsumata, Atsushi Ohori	Proof-Directed De-compilation of Low-Level Code.	ESOP	2001	DBLP DOI BibTeX RDF
32	Herman Geuvers, Freek Wiedijk, Jan Zwanenburg	A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals.	TYPES	2000	DBLP DOI BibTeX RDF
32	Herman Geuvers, Erik Poll, Jan Zwanenburg	Safe Proof Checking in Type Theory with Y.	CSL	1999	DBLP DOI BibTeX RDF
32	Kenneth L. McMillan	Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract).	FMCAD	1998	DBLP DOI BibTeX RDF
32	Andreas Weiermann	A proof of strongly uniform termination for Gödel's TT by methods from local predicativity.	Arch. Math. Log.	1997	DBLP DOI BibTeX RDF
32	Konrad Slind	A Parameterized Proof Manager.	TPHOLs	1994	DBLP DOI BibTeX RDF
31	David M. Goldschlag	Mechanically Verifying Concurrent Programs with the Boyer-Moore Prover.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	mechanically verifying concurrent programs, Boyer-Moore prover, transition system model, parallel programming, distributed algorithm, concurrency, theorem proving, program verification, safety, encoding, encoding, operational semantics, inference mechanisms, liveness, inference rules, proof system, Unity
31	Paul Brauner, Clément Houtmann, Claude Kirchner	Superdeduction at Work.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
31	Abdessamad Imine, Michaël Rusinowitch	Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
31	Jan Willem Klop, Vincent van Oostrom, Femke van Raamsdonk	Reduction Strategies and Acyclicity.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
31	Thomas Studer	Constructive Foundations for Featherweight Java.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF	reasoning about programs, explicit mathematics, object-oriented programming, denotational semantics, Featherweight Java
31	Peter Dybjer, Anton Setzer	Indexed Induction-Recursion.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF	Dependent type theory, Martin-Löf Type Theory, inductive-recursive definitions, inductive families, normalization proofs, generic programming, inductive definitions, initial algebras
31	Richard Mayr, Annette Schelten	Polynomial Time Approximation Schemes for Geometric Optimization Problems in Euclidean Metric Spaces.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
31	Volker Heun, Wolfgang Merkle, Ulrich Weigand	Proving the PCP-Theorem.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
31	Alexander Wolff 0001	The Hardness of Approximating Set Cover.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
31	Clemens Gröpl, Martin Skutella	Parallel Repetition of MIP(2, 1) Systems.	Lectures on Proof Verification and Approximation Algorithms	1997	DBLP DOI BibTeX RDF
31	Keita Xagawa, Keisuke Tanaka	Zero-Knowledge Protocols for NTRU: Application to Identification and Proof of Plaintext Knowledge.	ProvSec	2009	DBLP DOI BibTeX RDF	proof of plaintext knowledge, identification, code, zero knowledge, proof of knowledge, NTRU, lattice-based cryptography
31	Tom Coffey, Puneet Saidha, Peter Burrows	Analysing the security of a non-repudiation communication protocol with mandatory proof of receipt.	ISICT	2003	DBLP DOI BibTeX RDF	cryptographic protocol verification, logical postulates, proof of origin, proof of receipt, logics, security protocols, public-key cryptography, non-repudiation, deductive reasoning
31	Richard Bornat, Bernard Sufrin	A Minimal Graphical User Interface for the Jape Proof Calculator.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	GUI proof, Proof calculator
31	Scott D. Stoller	Addendum to "Proof Rules for Flush Channels".	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	flush channels, multiple identical messages, logic system, distributed systems, distributed processing, message passing, program verification, program verification, asynchronous communication, formal logic, channel, proof system, communicating processes, proof rules
31	John Watrous	Succinct quantum proofs for properties of finite groups.	FOCS	2000	DBLP DOI BibTeX RDF	succinct quantum proofs, finite group properties, quantum computational variant, quantum proof, quantum state, NP-type proof, black-box groups, group operations, group oracle, Group Non-Membership problem, bounded error, simple proof, quantum proofs, classical proofs, group properties, computational complexity, theorem proving, quantum computing, quantum computer, certificate, nondeterminism, polynomial time, strings, group theory, finite groups
30	Alfredo De Santis, Moti Yung	Crptograpic Applications of the Non-Interactive Metaproof and Many-Prover Systems.	CRYPTO	1990	DBLP DOI BibTeX RDF
30	Ilya Beylin, Peter Dybjer	Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids.	TYPES	1995	DBLP DOI BibTeX RDF
30	Heidar Pirzadeh, Danny Dubé	VEP: a virtual machine for extended proof-carrying code.	VMSec	2008	DBLP DOI BibTeX RDF	virtual machine, proof-carrying code
30	Tsuyoshi Ito, Hirotada Kobayashi, Daniel Preda, Xiaoming Sun 0001, Andrew Chi-Chih Yao	Generalized Tsirelson Inequalities, Commuting-Operator Provers, and Multi-prover Interactive Proof Systems.	CCC	2008	DBLP DOI BibTeX RDF	multi-prover interactive proof systems, quantum nonlocality, Tsirelson inequality, entanglement
30	Grigoris Antoniou, Antonis Bikakis, Polyvios Damianakis, Mixalhs Foukarakis, Giorgos Iacovidis, Marianna Karmazi, Haridimos Kondylakis, Antreas Makridakis, Giorgos Nikiforos, George Papadourakis, Manolis Papoutsakis, Aggeliki Psyharaki, Giorgos Stratakis, Panagiotis Tourlakis, Petros Tsialiamanis, Giorgos Vasiliadis, Gerd Wagner 0001, Dimitris Velegrakis	A Multi-agent Environment for Serving Proof Explanations in the Semantic Web.	SETN	2008	DBLP DOI BibTeX RDF	Proof Explanation, Semantic Web, Multi-agent Systems
30	Li Ye, Junliang Chen	Automatic Composition of Semantic Web Services - A Theorem Proof Approach.	ASWC	2006	DBLP DOI BibTeX RDF	Automatic Theorem Proof, Deductive Program Synthesis, Semantic Web Services, Automatic Service Composition
30	Takayuki Suyama, Makoto Yokoo	Strategy/False-name Proof Protocols for Combinatorial Multi-Attribute Procurement Auction.	Auton. Agents Multi Agent Syst.	2005	DBLP DOI BibTeX RDF	strategy/false-name proof, mechanism design, combinatorial auction, multi-attribute
30	Andrzej S. Murawski, C.-H. Luke Ong	Dominator Trees and Fast Verification of Proof Nets.	LICS	2000	DBLP DOI BibTeX RDF	verification of proof nets, Linear Logic, dominator trees
30	Sanjeev Arora, Carsten Lund, Rajeev Motwani 0001, Madhu Sudan 0001, Mario Szegedy	Proof Verification and the Hardness of Approximation Problems.	J. ACM	1998	DBLP DOI BibTeX RDF	optimization, NP-completeness, randomness, proof verification
30	Marvin R. G. Schiller, Christoph Benzmüller	Presenting Proofs with Adapted Granularity.	KI	2009	DBLP DOI BibTeX RDF	Adaptive proof presentation, proof tutoring, machine learning, granularity, automated reasoning
30	Andrew Ireland, Bill J. Ellis, Andrew Cook, Roderick Chapman, Janet Barnes	An Integrated Approach to High Integrity Software Verification.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	static analysis, SPARK, program proof, proof planning
30	Dieter Fensel, Arno Schönegge	Using KIV to Specify and Verify Architectures of Knowledge-Based Systems.	ASE	1997	DBLP DOI BibTeX RDF	reusable elements, Karlsruhe interactive verifier, algorithmic specification, interactive theorem prover, proof management, proof reuse, formal specification, formal specifications, knowledge-based systems, specification language, abstract data types, dynamic logic, functional specification
29	Cristian S. Calude, Christine Müller	Formal Proof: Reconciling Correctness and Understanding.	Calculemus/MKM	2009	DBLP DOI BibTeX RDF
29	Atsushi Ohori	A proof theory for machine code.	ACM Trans. Program. Lang. Syst.	2007	DBLP DOI BibTeX RDF	Curry-Howard isomorphism
29	Jahn-Takeshi Saito, Guillaume Chaslot, Jos W. H. M. Uiterwijk, H. Jaap van den Herik	Monte-Carlo Proof-Number Search for Computer Go.	Computers and Games	2006	DBLP DOI BibTeX RDF
29	Chris Hunter, Peter J. Robinson 0001, Paul A. Strooper	Flexible Proof Reuse for Software Verification.	AMAST	2004	DBLP DOI BibTeX RDF
29	Bernhard Beckert, Vladimir Klebanov	Proof Reuse for Deductive Program Verification.	SEFM	2004	DBLP DOI BibTeX RDF
29	Hirotada Kobayashi, Keiji Matsumoto, Tomoyuki Yamakami	Quantum Merlin-Arthur Proof Systems: Are Multiple Merlins More Helpful to Arthur?	ISAAC	2003	DBLP DOI BibTeX RDF
29	Louise A. Dennis, Alan Bundy	A Comparison of Two Proof Critics: Power vs. Robustness.	TPHOLs	2002	DBLP DOI BibTeX RDF
29	Guillaume Lussier, Hélène Waeselynck	Informal Proof Analysis Towards Testing Enhancement.	ISSRE	2002	DBLP DOI BibTeX RDF
29	Gianluigi Bellin, Arnaud Fleury	Planar and braided proof-nets for multiplicative linear logic with mix.	Arch. Math. Log.	1998	DBLP DOI BibTeX RDF
29	David J. Pym, Lincoln A. Wallen	Investigations into Proof-Search in a System of First-Order Dependent Function Types.	CADE	1990	DBLP DOI BibTeX RDF
29	Andreas Goerdt	Cuting Plane Versus Frege Proof Systems.	CSL	1990	DBLP DOI BibTeX RDF
28	László Babai, Peter G. Kimmel	Randomized Simultaneous Messages: Solution of a Problem of Yao in Communication Complexity.	CCC	1997	DBLP DOI BibTeX RDF	randomized simultaneous messages, two-player communication model, deterministic SM complexity, quadratic reduction, lower bound proof, computational complexity, communication complexity, linear algebra
28	Alan Bundy	The Use of Explicit Plans to Guide Inductive Proofs.	CADE	1988	DBLP DOI BibTeX RDF	inductive proofs, formal methods, planning, theorem proving, automatic programming, Proof plans
28	Gabriele Usberti	The Paradox of Knowability from an Intuitionistic Standpoint.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
28	Jan Ekman	Self-contradictory Reasoning.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
28	Walter Dean, Hidenori Kurokawa	Kreisel's Theory of Constructions, the Kreisel-Goodman Paradox, and the Second Clause.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
28	Kosta Dosen	On the Paths of Categories.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
28	Jan von Plato	Explicit Composition and Its Application in Proofs of Normalization.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
28	Dag Prawitz	On the Relation Between Heyting's and Gentzen's Approaches to Meaning.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
28	Kosta Dosen	Comments on an Opinion.	Advances in Proof-Theoretic Semantics	2016	DBLP DOI BibTeX RDF
28	Petr Hájek 0001	Deductive Systems of Fuzzy Logic.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	K. Ramasubramanian	History and Development of Indian Logic: An Overview.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	John N. Crossley	What Is Mathematical Logic? A Survey.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Wilfrid Hodges	A Visit to Tarski's Seminar on Elimination of Quantifiers.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Noson S. Yanofsky	An Introduction to Quantum Computing.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Ron van der Meyden	Two Applications of Epistemic Logic in Computer Security.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Eric Pacuit	Towards a Logical Analysis of Adjusted Winner.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Johan van Benthem	Logic Games: From Tools to Models of Interaction.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	G. Venkatesh	Temporal Logic with Preferences and Reasoning About Games.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	B. Devadas Acharya, Shalini Joshi	Some Reflections on Discrete Mathematical Models in Behavioral, Cognitive and Social Sciences.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	K. Ramasubramanian	The Concept of Hetvābhāsa in Nyāya-śāstra.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Ferdinando Cicalese, Daniele Mundici	Recent Developments of Feedback Coding and Its Relations with Many-Valued Logic.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Rohit Parikh	Is There a Logic of Society?	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Krister Segerberg	In memory of Jasu Magan Bhana Panchia (1963-1991): Iterated Belief Revision in Dynamic Doxastic Logic.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	John N. Crossley	What Is the Difference Between Proofs and Programs?	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Andreas Blass, Yuri Gurevich	Zero-One Laws: Thesauri and Parametric Conditions.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Sundar Sarukkai	Indian Logic and Philosophy of Science: The Logic-Epistemology Link.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Wilfrid Hodges	From Sentence Meanings to Full Semantics.	Proof, Computation and Agency	2011	DBLP DOI BibTeX RDF
28	Stefano Aguzzoli, Agata Ciabattoni, Brunella Gerla, Corrado Manara, Vincenzo Marra (eds.)	Algebraic and Proof-theoretic Aspects of Non-classical Logics, Papers in Honor of Daniele Mundici on the Occasion of His 60th birthday	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2007	DBLP DOI BibTeX RDF
28	Hubert Comon-Lundh, Claude Kirchner, Hélène Kirchner (eds.)	Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
28	Claude Marché	Towards Modular Algebraic Specifications for Pointer Programs: A Case Study.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
28	Cristina Borralleras, Albert Rubio	Orderings and Constraints: Theory and Practice of Proving Termination.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
28	Sergiu Bursuc, Hubert Comon-Lundh, Stéphanie Delaune	Deducibility Constraints, Equational Theory and Electronic Money.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
28	Evelyne Contejean	Modeling Permutations in Coqfor Coccinelle.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
28	Frédéric Blanqui	Computability Closure: Ten Years Later.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
28	Sandra Alves, Maribel Fernández, Mário Florido, Ian Mackie	Linear Recursive Functions.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF	linear calculi, computable functions, iteration, Recursion theory
28	Nachum Dershowitz, Georg Moser	The Hydra Battle Revisited.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
28	Jacek Chrzaszcz, Daria Walukiewicz-Chrzaszcz	Towards Rewriting in Coq.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
28	Francesc Esteva, Lluís Godo	Towards the Generalization of Mundici's Gamma Functor to IMTL Algebras: The Linearly Ordered Case.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Maria Luisa Dalla Chiara, Roberto Giuntini, Roberto Leporini	Reversibility and Irreversibility in Quantum Computation and in Quantum Computational Logics.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Franco Montagna	Notes on Strong Completeness in Lukasiewicz, Product and BL Logics and in Their First-Order Extensions.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Beloslav Riecan	Probability Theory on IF Events.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Arnon Avron, Anna Zamansky	Many-Valued Non-deterministic Semantics for First-Order Logics of Formal (In)consistency.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Antonio Di Nola, Mirko Navara	Cantor-Bernstein Property for MV-Algebras.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Matthias Baaz	Note on Conditional Constructivity.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Giovanni Panti	The Automorphism Group of Falsum-Free Product Logic.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Costas A. Drossos, Panagis Karazeris	A Note on Representing and Interpreting MV-Algebras.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Xavier Caicedo	Implicit Operations in MV-Algebras and the Connectives of Lukasiewicz Logic.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Lawrence Peter Belluce, Antonio Di Nola, Ada Lettieri	Symmetric MV-Algebras.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Roberto Cignoli	The Algebras of Lukasiewicz Many-Valued Logic: A Historical Overview.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Andrew M. W. Glass, Françoise Point	Finitely Presented Abelian Lattice-Ordered Groups.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Petr Hájek 0001	On Fuzzy Theories with Crisp Sentences.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
28	Birgit Elbl	Modeling Meta-logical Features in a Calculus with Frozen Variables.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF	logic programming, control, substructural logic
28	Peter H. Schmitt	Iterate Logic.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF
28	Klaus Aehlig, Jan Johannsen, Helmut Schwichtenberg, Sebastiaan Terwijn	Linear Ramified Higher Type Recursion and Parallel Complexity.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF	higher types, parallel computation, recursion, linear logic, lambda calculus, implicit computational complexity, NC
28	Ralph Matthes	Interpolation for Natural Deduction with Generalized Eliminations.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF