Search results for "prover"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
115	Subhash Khot	On the Power of Unique 2-Prover 1-Round Games.	CCC	2002	DBLP DOI BibTeX RDF	2-prover games, Hardness of approximation, probabilistically checkable proofs
100	Ian Agol, Joel Hass, William P. Thurston	3-MANIFOLD KNOT GENUS is NP-complete.	CCC	2002	DBLP DOI BibTeX RDF	2-prover games, Hardness of approximation, probabilistically checkable proofs
98	Subhash Khot	On the power of unique 2-prover 1-round games.	STOC	2002	DBLP DOI BibTeX RDF
78	Boutheina Chetali	Formal Verification of Concurrent Programs Using the Larch Prover.	IEEE Trans. Software Eng.	1998	DBLP DOI BibTeX RDF	theorem prover methodology, Larch prover, computer-checked proof, Formal verification, communication protocol, protocol verification, UNITY
74	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
62	Joe Kilian, Ronitt Rubinfeld	Interactive Proofs with Space Bounded Provers.	CRYPTO	1991	DBLP DOI BibTeX RDF
53	Serge Mechveliani	From a Computer Algebra Library to a System with an Equational Prover.	AISC	2004	DBLP DOI BibTeX RDF	equational prover, term rewriting, computer algebra
53	Dipankar Sarkar 0001, S. C. De Sarkar	A Theorem Prover for Verifying Iterative Programs Over Integers.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	rule-based theorem prover, iterative programs, overall proof construction strategy, array-sorting program, expert systems, theorem proving, program verification, performance measures, iterative methods, correctness proofs
50	László Babai, Lance Fortnow, Carsten Lund	Non-Deterministic Exponential Time Has Two-Prover Interactive Protocols	FOCS	1990	DBLP DOI BibTeX RDF	efficient provability, multiple prover interactive proof systems, two-prover interactive protocols, noncommunicating provers, randomizing polynomial-time verifier, coNP-complete languages, nondeterministic exponential time, polynomial time
50	Julia Kempe, Hirotada Kobayashi, Keiji Matsumoto, Thomas Vidick	Using Entanglement in Quantum Multi-Prover Interactive Proofs.	Comput. Complex.	2009	DBLP DOI BibTeX RDF	Subject classification. 03D15, 81P68, 68Q15, 68Q10
50	Julia Kempe, Hirotada Kobayashi, Keiji Matsumoto, Thomas Vidick	Using Entanglement in Quantum Multi-prover Interactive Proofs.	CCC	2008	DBLP DOI BibTeX RDF	quantum interactive proofs, public-coin, parallelization, entanglement
50	Adolfo Gustavo Serra Seca Neto, Marcelo Finger	Effective Prover for Minimal Inconsistency Logic.	IFIP AI	2006	DBLP DOI BibTeX RDF
50	Yoshinao Isobe, Markus Roggenbach	A Generic Theorem Prover of CSP Refinement.	TACAS	2005	DBLP DOI BibTeX RDF
50	Hirotada Kobayashi, Keiji Matsumoto	Quantum Multi-prover Interactive Proof Systems with Limited Prior Entanglement.	ISAAC	2002	DBLP DOI BibTeX RDF
50	George C. Necula, Peter Lee 0001	Proof Generation in the Touchstone Theorem Prover.	CADE	2000	DBLP DOI BibTeX RDF
50	Shang-Ching Chou	A Geometry Theorem Prover for Macintoshes.	CADE	1992	DBLP DOI BibTeX RDF
50	Robert S. Boyer, J Strother Moore	A Theorem Prover for a Computational Logic.	CADE	1990	DBLP DOI BibTeX RDF
49	Boutheina Chetali, Barbara Heyd	Formal Verification of Concurrent Programs in LP and in COQ: A Comparative Analysis.	TPHOLs	1997	DBLP DOI BibTeX RDF	theorem prover methodology, Larch Prover, Computer Checked Proof, Formal Verification, Unity, Coq
46	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
46	Stefan Gerberding	DT - An Automated Theorem Prover for Multiple-Valued First-Order Predicate Logics.	ISMVL	1996	DBLP DOI BibTeX RDF	Deep Thought, multiple-valued first-order logics, lemma generation, tableau expansion, branch closure, theorem proving, multivalued logic, multiple-valued logics, quantifiers, first-order predicate logic, truth tables, automated theorem prover
44	Mark T. Vandevoorde, Deepak Kapur	Distributed Larch Prover (DLP): An Experiment in Parallelizing a Rewrite-Rule Based Prover.	RTA	1996	DBLP DOI BibTeX RDF
43	K. Subramani 0001	A Randomized Algorithm for BBCSPs in the Prover-Verifier Model.	ICTAC	2007	DBLP DOI BibTeX RDF
43	Wolfgang Windsteiger	A Set Theory Prover Within Theorema.	EUROCAST	2001	DBLP DOI BibTeX RDF
43	Deepak Kapur, Mahadevan Subramaniam	Using an induction prover for verifying arithmetic circuits.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	Induction, Automated reasoning, Decision procedures, Rewriting, Arithmetic circuits, Hardware verification
43	Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt	System Description: card TAP: The First Theorem Prover on a Smart Card.	CADE	1998	DBLP DOI BibTeX RDF
43	Chae Hoon Lim, Pil Joong Lee	Server (Prover/Signer)-Aided Verification of Identity Proofs and Signatures.	EUROCRYPT	1995	DBLP DOI BibTeX RDF
42	Raul H. C. Lopes, Mark Tarver	Inducing Theorem Provers from Proofs.	ICTAI	1997	DBLP DOI BibTeX RDF	theorem prover induction, automatic theorem prover generation, proof examples, intuitionistic propositional calculus, depth-first search strategy, loop detection, inductive generalization, machine learning, theorem proving
42	Anand Chavan, Shiu-Kai Chin, Shahid Ikram, Jang Dae Kim, Juin-Yeu Zu	Extending VLSI design with higher-order logic.	ICCD	1995	DBLP DOI BibTeX RDF	Cambridge Higher-Order Logic theorem-prover, microprogram sequencer, Am2910, VLSI, formal verification, formal verification, logic testing, theorem proving, logic design, logic CAD, VLSI design, higher-order logic, theorem-prover, design environment, instruction-set architecture, VLSI CAD
41	Takahito Aoto 0001, Junichi Yoshida, Yoshihito Toyama	Proving Confluence of Term Rewriting Systems Automatically.	RTA	2009	DBLP DOI BibTeX RDF
41	Adnan Vora, Mikhail Nesterenko	Secure Location Verification Using Radio Broadcast.	IEEE Trans. Dependable Secur. Comput.	2006	DBLP DOI BibTeX RDF	security, wireless sensor networks, Location verification
41	Adnan Vora, Mikhail Nesterenko	Secure Location Verification Using Radio Broadcast.	OPODIS	2004	DBLP DOI BibTeX RDF	security, wireless sensor networks, location verification
40	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
38	Viktor K. Sabelfeld, Kai Kapp	Numeric Types in Formal Synthesis.	Ershov Memorial Conference	2003	DBLP DOI BibTeX RDF	correct hardware synthesis, formal specification, higher-order logic, theorem prover, arithmetic operations
37	Kenneth Roe	The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover.	CAV	2006	DBLP DOI BibTeX RDF
36	Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane	Reachability analysis using multiway decision graphs in the HOL theorem prover.	SAC	2008	DBLP DOI BibTeX RDF	reachability analysis, HOL, multiway decision graphs
36	Joseph P. Near, William E. Byrd, Daniel P. Friedman	alpha-leanTAP: A Declarative Theorem Prover for First-Order Classical Logic.	ICLP	2008	DBLP DOI BibTeX RDF
36	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
36	Jun Sawada, Erik Reeber	ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool.	FMCAD	2006	DBLP DOI BibTeX RDF
36	Virginie Thion, Serenella Cerrito, Marta Cialdea Mayer	A General Theorem Prover for Quantified Modal Logics.	TABLEAUX	2002	DBLP DOI BibTeX RDF
36	Tanel Tammet	A Resolution Theorem Prover for Intuitonistic Logic.	CADE	1996	DBLP DOI BibTeX RDF
36	Cynthia Dwork, Uriel Feige, Joe Kilian, Moni Naor, Shmuel Safra	Low Communication 2-Prover Zero-Knowledge Proofs for NP.	CRYPTO	1992	DBLP DOI BibTeX RDF
36	Blayne E. Mayfield, Timothy B. Baird	STP: A Simple Theorem Prover for IBM-PC Compatible Computers.	SIGSMALL/PC Symposium	1990	DBLP DOI BibTeX RDF	IBM PC, Turbo Pascal
34	Kotaro Sonoda, Osamu Takizawa	User Authentication Scheme Using Individual Auditory Pop-Out.	New Directions in Intelligent Interactive Multimedia	2008	DBLP DOI BibTeX RDF
34	Ivan Damgård, Jesper Buus Nielsen, Daniel Wichs	Isolated Proofs of Knowledge and Isolated Zero Knowledge.	EUROCRYPT	2008	DBLP DOI BibTeX RDF
34	Quoc Bao Vo	A task-oriented agent-based mechanism for theorem proving.	IAT	2003	DBLP DOI BibTeX RDF
34	Paolo Traverso, Piergiorgio Bertoli	Mechanized result verification: an industrial application.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	Mechanized result verification, Online/offline checking, Validation, Decomposition, Safety critical software
34	Maarten de Mol, Marko C. J. D. van Eekelen	A Proof Tool Dedicated to Clean - The First Prototype.	AGTIVE	1999	DBLP DOI BibTeX RDF
33	Sa'ed Abed, Otmane Aït Mohamed	MDGs Reduction Technique Based on the HOL Theorem Prover.	ISMVL	2010	DBLP DOI BibTeX RDF	Soundness, Reduction Techniques, Multiway Decision Graphs, HOL Theorem Prover
33	Dror Lapidot, Adi Shamir	Fully Parallelized Multi Prover Protocols for NEXP-Time (Extended Abstract)	FOCS	1991	DBLP DOI BibTeX RDF	one-round perfect zero-knowledge protocol, fully parallelized multi prover protocols, NEXP-time, language, parallel executions
31	Marcel Oliveira, Ana Cavalcanti 0001, Jim Woodcock 0001	Unifying Theories in ProofPower-Z.	UTP	2006	DBLP DOI BibTeX RDF	Unifying Theories of Programming, theorem prover
31	Mizuhito Ogawa, Eiichi Horita, Satoshi Ono	Proving Properties of Incremental Merkle Trees.	CADE	2005	DBLP DOI BibTeX RDF	temporal authentication, theorem prover, Merkle tree
31	Kun Wei, James Heather	Embedding the Stable Failures Model of CSP in PVS.	IFM	2005	DBLP DOI BibTeX RDF	CSP, deadlock, determinism, liveness, theorem prover
31	Johann Schumann, Bernd Fischer 0002	NORA/HAMMR: Making Deduction-Based Software Component Retrieval Practical.	ASE	1997	DBLP DOI BibTeX RDF	deduction-based software component retrieval, NORA/HAMMR, search keys, proof tasks, rejection filters, model checking techniques, confirmation filter, software reusability, signature matching, automated theorem prover
30	Mario Carneiro	Metamath Zero: Designing a Theorem Prover Prover.	CICM	2020	DBLP DOI BibTeX RDF
30	Mihir Parang Mehta	Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32.	ACL2	2018	DBLP DOI BibTeX RDF
30	Shuling Wang, Naijun Zhan, Liang Zou	An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems.	ICFEM	2015	DBLP DOI BibTeX RDF
30	Gábor Tardos	Multi-prover Encoding Schemes and Three-prover Proof Systems.	J. Comput. Syst. Sci.	1996	DBLP DOI BibTeX RDF
30	Gábor Tardos	Multi-Prover Encoding Schemes and Three-Prover Proof Systems.	SCT	1994	DBLP DOI BibTeX RDF
30	Aleksandar Krapez, Miodrag Kapetanovic, Zoran Ognjanovic, Tatjana Petrovic	Prover 91 - A Parallel Theorem Prover (Extended Abstract).	TABLEAUX	1992	DBLP BibTeX RDF
30	Steven Greenbaum, David A. Plaisted	The Illinois Prover: A General Purpose Resolution Theorem Prover.	CADE	1986	DBLP DOI BibTeX RDF
30	Shang-Ching Chou	GEO-Prover - A Geometry Theorem Prover Developed at UT.	CADE	1986	DBLP DOI BibTeX RDF
29	Hicham Bensaid, Ricardo Caferra, Nicolas Peltier	Dei: A Theorem Prover for Terms with Integer Exponents.	CADE	2009	DBLP DOI BibTeX RDF
29	Dru McCandless, Leo Obrst, Shayn Hawthorne	Dynamic Web Service Assembly Using OWL and a Theorem Prover.	ICSC	2009	DBLP DOI BibTeX RDF
29	Laura I. Meikle, Jacques D. Fleuriot	Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B.	CAV	2008	DBLP DOI BibTeX RDF
29	André Platzer, Jan-David Quesel	KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description).	IJCAR	2008	DBLP DOI BibTeX RDF	verification of hybrid systems, decision procedures, computer algebra, automated theorem proving, dynamic logic
29	Kenneth L. McMillan	Quantified Invariant Generation Using an Interpolating Saturation Prover.	TACAS	2008	DBLP DOI BibTeX RDF
29	Aaron Richard Coble	Formalized Information-Theoretic Proofs of Privacy Using the HOL4 Theorem-Prover.	Privacy Enhancing Technologies	2008	DBLP DOI BibTeX RDF
29	Laura I. Meikle, Jacques D. Fleuriot	Combining Isabelle and QEPCAD-B in the Prover's Palette.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF
29	Richard Bonichon, David Delahaye, Damien Doligez	Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs.	LPAR	2007	DBLP DOI BibTeX RDF
29	Behzad Akbarpour, Lawrence C. Paulson	Extending a Resolution Prover for Inequalities on Elementary Functions.	LPAR	2007	DBLP DOI BibTeX RDF
29	Christian Böhm 0001, Michael Gruber, Peter Kunath, Alexey Pryakhin, Matthias Schubert	ProVeR: Probabilistic Video Retrieval using the Gauss-Tree.	ICDE	2007	DBLP DOI BibTeX RDF
29	José-Antonio Alonso, Joaquín Borrego-Díaz, María-José Hidalgo, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina	A Formally Verified Prover for the ALC Description Logic.	TPHOLs	2007	DBLP DOI BibTeX RDF
29	Shinya Umeno, Nancy A. Lynch	Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study.	FM	2006	DBLP DOI BibTeX RDF
29	Tadashi Takahashi, Hidetsune Kobayashi	The Effect of the Theorem Prover in Cognitive Science.	International Conference on Computational Science (1)	2006	DBLP DOI BibTeX RDF
29	Giuseppe Persiano, Ivan Visconti	Single-Prover Concurrent Zero Knowledge in Almost Constant Rounds.	ICALP	2005	DBLP DOI BibTeX RDF
29	Kaustuv Chaudhuri, Frank Pfenning	A Focusing Inverse Method Theorem Prover for First-Order Linear Logic.	CADE	2005	DBLP DOI BibTeX RDF
29	Andreas Abel 0001, Thierry Coquand, Ulf Norell	Connecting a Logical Framework to a First-Order Logic Prover.	FroCoS	2005	DBLP DOI BibTeX RDF
29	Kenneth L. McMillan	An Interpolating Theorem Prover.	TACAS	2004	DBLP DOI BibTeX RDF
29	Nicola Olivetti, Gian Luca Pozzato	CondLean: A Theorem Prover for Conditional Logics.	TABLEAUX	2003	DBLP DOI BibTeX RDF
29	Joshua S. Hodas, Naoyuki Tamura	lolliCop - A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic.	IJCAR	2001	DBLP DOI BibTeX RDF
29	Jens Happe	The MODPROF Theorem Prover.	IJCAR	2001	DBLP DOI BibTeX RDF
29	David Spelt, Susan Even	A Theorem Prover-Based Analysis Tool for Object-Oriented Databases.	TACAS	1999	DBLP DOI BibTeX RDF
29	David S. Hardin, Matthew Wilding, David A. Greve	Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle.	CAV	1998	DBLP DOI BibTeX RDF
29	Michel Levy	Prover KT4.	TABLEAUX	1998	DBLP DOI BibTeX RDF
29	Yves Ledru	Identifying Pre-Conditions with the Z/EVES Theorem Prover.	ASE	1998	DBLP DOI BibTeX RDF
29	Maria Paola Bonacina	The Clause-Diffusion Theorem Prover Peers-mcd (System Description).	CADE	1997	DBLP DOI BibTeX RDF
29	Scott Hazelhurst, Carl-Johan H. Seger	A simple theorem prover based on symbolic trajectory evaluation and BDD's.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	1995	DBLP DOI BibTeX RDF
29	Peter Baumgartner 0001, Ulrich Furbach	PROTEIN: A PROver with a Theory Extension INterface.	CADE	1994	DBLP DOI BibTeX RDF
29	Maria Paola Bonacina, Jieh Hsiang	Distributed Deduction by Clause-Diffusion: The Aquarius Prover.	DISCO	1993	DBLP DOI BibTeX RDF
29	Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita 0002	MGTP: A Parallel Theorem Prover Based on Lazy Model Generation.	CADE	1992	DBLP DOI BibTeX RDF
29	Aline Deruyver	EMMY: A Refutational Theorem Prover for First-Order Logic with Equation.	RTA	1991	DBLP DOI BibTeX RDF
29	Dror Lapidot, Adi Shamir	A One-Round, Two-Prover, Zero-Knowledge Protocol for NP.	CRYPTO	1991	DBLP DOI BibTeX RDF
29	Larry M. Hines	Str+ve-Subset: The Str+ve-based Subset Prover.	CADE	1990	DBLP DOI BibTeX RDF
29	Mark Tarver	An Examination of the Prolog Technology Theorem-Prover.	CADE	1990	DBLP DOI BibTeX RDF	PTTP, metalevel reasoning, Prolog Normal Form, refinement
29	Johann Schumann, Reinhold Letz	PARTHEO: A High-Performance Parallel Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF	Warren Abstract Machine, message passing, Theorem proving, first-order logic, transputers, or-parallelism, model elimination, connection method
29	Alfredo De Santis, Moti Yung	Crptograpic Applications of the Non-Interactive Metaproof and Many-Prover Systems.	CRYPTO	1990	DBLP DOI BibTeX RDF
29	Heikki Tuominen	Proving Properties of Elementary Net Systems with a Special-Purpose Theorem Prover.	Automatic Verification Methods for Finite State Systems	1989	DBLP DOI BibTeX RDF
29	Michael Ben-Or, Shafi Goldwasser, Joe Kilian, Avi Wigderson	Efficient Identification Schemes Using Two Prover Interactive Proofs.	CRYPTO	1989	DBLP DOI BibTeX RDF
29	Mark E. Stickel	A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler.	CADE	1986	DBLP DOI BibTeX RDF
29	Paul Y. Gloess	An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions.	CADE	1980	DBLP DOI BibTeX RDF