|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 1388 occurrences of 676 keywords
|
|
|
Results
Found 2141 publication records. Showing 2141 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
115 | Subhash Khot |
On the Power of Unique 2-Prover 1-Round Games. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CCC ![In: Proceedings of the 17th Annual IEEE Conference on Computational Complexity, Montréal, Québec, Canada, May 21-24, 2002, pp. 25, 2002, IEEE Computer Society, 0-7695-1468-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CCC ![In: Proceedings of the 17th Annual IEEE Conference on Computational Complexity, Montréal, Québec, Canada, May 21-24, 2002, pp. 24, 2002, IEEE Computer Society, 0-7695-1468-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STOC ![In: Proceedings on 34th Annual ACM Symposium on Theory of Computing, May 19-21, 2002, Montréal, Québec, Canada, pp. 767-775, 2002, ACM, 1-58113-495-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
78 | Boutheina Chetali |
Formal Verification of Concurrent Programs Using the Larch Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 24(1), pp. 46-62, 1998. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CCC ![In: Proceedings of the 23rd Annual IEEE Conference on Computational Complexity, CCC 2008, 23-26 June 2008, College Park, Maryland, USA, pp. 187-198, 2008, IEEE Computer Society, 978-0-7695-3169-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CRYPTO ![In: Advances in Cryptology - CRYPTO '91, 11th Annual International Cryptology Conference, Santa Barbara, California, USA, August 11-15, 1991, Proceedings, pp. 225-231, 1991, Springer, 3-540-55188-3. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
53 | Serge Mechveliani |
From a Computer Algebra Library to a System with an Equational Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISC ![In: Artificial Intelligence and Symbolic Computation, 7th International Conference, AISC 2004, Linz, Austria, September 22-24, 2004, Proceedings, pp. 281-284, 2004, Springer, 3-540-23212-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 15(12), pp. 1550-1566, 1989. The full citation details ...](Pics/full.jpeg) |
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 ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 31st Annual Symposium on Foundations of Computer Science, St. Louis, Missouri, USA, October 22-24, 1990, Volume I, pp. 16-25, 1990, IEEE Computer Society, 0-8186-2082-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. Complex. ![In: Comput. Complex. 18(2), pp. 273-307, 2009. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CCC ![In: Proceedings of the 23rd Annual IEEE Conference on Computational Complexity, CCC 2008, 23-26 June 2008, College Park, Maryland, USA, pp. 211-222, 2008, IEEE Computer Society, 978-0-7695-3169-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFIP AI ![In: Artificial Intelligence in Theory and Practice, IFIP 19th World Computer Congress, TC 12: IFIP AI 2006 Stream, August 21-24, 2006, Santiago, Chile, pp. 465-474, 2006, Springer, 0-387-34654-6. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
50 | Yoshinao Isobe, Markus Roggenbach |
A Generic Theorem Prover of CSP Refinement. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, pp. 108-123, 2005, Springer, 3-540-25333-5. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
50 | Hirotada Kobayashi, Keiji Matsumoto |
Quantum Multi-prover Interactive Proof Systems with Limited Prior Entanglement. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISAAC ![In: Algorithms and Computation, 13th International Symposium, ISAAC 2002 Vancouver, BC, Canada, November 21-23, 2002, Proceedings, pp. 115-127, 2002, Springer, 3-540-00142-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
50 | George C. Necula, Peter Lee 0001 |
Proof Generation in the Touchstone Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, pp. 25-44, 2000, Springer, 3-540-67664-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
50 | Shang-Ching Chou |
A Geometry Theorem Prover for Macintoshes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, pp. 686-690, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
50 | Robert S. Boyer, J Strother Moore |
A Theorem Prover for a Computational Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 1-15, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
49 | Boutheina Chetali, Barbara Heyd |
Formal Verification of Concurrent Programs in LP and in COQ: A Comparative Analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, pp. 69-85, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CCC ![In: Proceedings of the 23rd Annual IEEE Conference on Computational Complexity, CCC 2008, 23-26 June 2008, College Park, Maryland, USA, pp. 199-210, 2008, IEEE Computer Society, 978-0-7695-3169-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMVL ![In: 26th IEEE International Symposium on Multiple-Valued Logic, ISMVL 1996, Santiago de Compostela, Spain, May 29-31, 1996, Proceedings, pp. 284-289, 1996, IEEE Computer Society, 0-8186-7392-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings, pp. 420-423, 1996, Springer, 3-540-61464-8. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
43 | K. Subramani 0001 |
A Randomized Algorithm for BBCSPs in the Prover-Verifier Model. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAC ![In: Theoretical Aspects of Computing - ICTAC 2007, 4th International Colloquium, Macau, China, September 26-28, 2007, Proceedings, pp. 455-466, 2007, Springer, 978-3-540-75290-5. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
43 | Wolfgang Windsteiger |
A Set Theory Prover Within Theorema. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCAST ![In: Computer Aided Systems Theory - EUROCAST 2001, Las Palmas de Gran Canaria, Spain, February 19-23, 2001, Revised Papers, pp. 525-539, 2001, Springer, 3-540-42959-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
43 | Deepak Kapur, Mahadevan Subramaniam |
Using an induction prover for verifying arithmetic circuits. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 3(1), pp. 32-65, 2000. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings, pp. 47-50, 1998, Springer, 3-540-64675-2. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
43 | Chae Hoon Lim, Pil Joong Lee |
Server (Prover/Signer)-Aided Verification of Identity Proofs and Signatures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCRYPT ![In: Advances in Cryptology - EUROCRYPT '95, International Conference on the Theory and Application of Cryptographic Techniques, Saint-Malo, France, May 21-25, 1995, Proceeding, pp. 64-78, 1995, Springer, 3-540-59409-4. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
42 | Raul H. C. Lopes, Mark Tarver |
Inducing Theorem Provers from Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAI ![In: 9th International Conference on Tools with Artificial Intelligence, ICTAI '97, Newport Beach, CA, USA, November 3-8, 1997, pp. 157-164, 1997, IEEE Computer Society, 0-8186-8203-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCD ![In: 1995 International Conference on Computer Design (ICCD '95), VLSI in Computers and Processors, October 2-4, 1995, Austin, TX, USA, Proceedings, pp. 85-94, 1995, IEEE Computer Society, 0-8186-7165-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings, pp. 93-102, 2009, Springer, 978-3-642-02347-7. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
41 | Adnan Vora, Mikhail Nesterenko |
Secure Location Verification Using Radio Broadcast. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Dependable Secur. Comput. ![In: IEEE Trans. Dependable Secur. Comput. 3(4), pp. 377-385, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
security, wireless sensor networks, Location verification |
41 | Adnan Vora, Mikhail Nesterenko |
Secure Location Verification Using Radio Broadcast. ![Search on Bibsonomy](Pics/bibsonomy.png) |
OPODIS ![In: Principles of Distributed Systems, 8th International Conference, OPODIS 2004, Grenoble, France, December 15-17, 2004, Revised Selected Papers, pp. 369-383, 2004, Springer, 3-540-27324-7. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
security, wireless sensor networks, location verification |
40 | David M. Goldschlag |
Mechanically Verifying Concurrent Programs with the Boyer-Moore Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 16(9), pp. 1005-1023, 1990. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Ershov Memorial Conference ![In: Perspectives of Systems Informatics, 5th International Andrei Ershov Memorial Conference, PSI 2003, Akademgorodok, Novosibirsk, Russia, July 9-12, 2003, Revised Papers, pp. 79-90, 2003, Springer, 3-540-20813-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 467-470, 2006, Springer, 3-540-37406-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2008 ACM Symposium on Applied Computing (SAC), Fortaleza, Ceara, Brazil, March 16-20, 2008, pp. 333-338, 2008, ACM, 978-1-59593-753-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICLP ![In: Logic Programming, 24th International Conference, ICLP 2008, Udine, Italy, December 9-13 2008, Proceedings, pp. 238-252, 2008, Springer, 978-3-540-89981-5. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
36 | Abdessamad Imine, Michaël Rusinowitch |
Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Rewriting, Computation and Proof ![In: Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, pp. 213-234, 2007, Springer, 978-3-540-73146-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
36 | Jun Sawada, Erik Reeber |
ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Formal Methods in Computer-Aided Design, 6th International Conference, FMCAD 2006, San Jose, California, USA, November 12-16, 2006, Proceedings, pp. 161-170, 2006, IEEE Computer Society, 0-7695-2707-8. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
36 | Virginie Thion, Serenella Cerrito, Marta Cialdea Mayer |
A General Theorem Prover for Quantified Modal Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2002, Copenhagen, Denmark, July 30 - August 1, 2002, Proceedings, pp. 266-280, 2002, Springer, 3-540-43929-3. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
36 | Tanel Tammet |
A Resolution Theorem Prover for Intuitonistic Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings, pp. 2-16, 1996, Springer, 3-540-61511-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CRYPTO ![In: Advances in Cryptology - CRYPTO '92, 12th Annual International Cryptology Conference, Santa Barbara, California, USA, August 16-20, 1992, Proceedings, pp. 215-227, 1992, Springer, 3-540-57340-2. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
36 | Blayne E. Mayfield, Timothy B. Baird |
STP: A Simple Theorem Prover for IBM-PC Compatible Computers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SIGSMALL/PC Symposium ![In: Proceedings of the 1990 ACM SIGSMALL/PC Symposium on Small Systems, March 28-30, 1990. Crystal City, VA, USA, pp. 98-105, 1990, ACM, 0-89791-347-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
IBM PC, Turbo Pascal |
34 | Kotaro Sonoda, Osamu Takizawa |
User Authentication Scheme Using Individual Auditory Pop-Out. ![Search on Bibsonomy](Pics/bibsonomy.png) |
New Directions in Intelligent Interactive Multimedia ![In: New Directions in Intelligent Interactive Multimedia, pp. 341-349, 2008, Springer, 978-3-540-68126-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
34 | Ivan Damgård, Jesper Buus Nielsen, Daniel Wichs |
Isolated Proofs of Knowledge and Isolated Zero Knowledge. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCRYPT ![In: Advances in Cryptology - EUROCRYPT 2008, 27th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Istanbul, Turkey, April 13-17, 2008. Proceedings, pp. 509-526, 2008, Springer, 978-3-540-78966-6. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
34 | Quoc Bao Vo |
A task-oriented agent-based mechanism for theorem proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IAT ![In: 2003 IEEE/WIC International Conference on Intelligent Agent Technology (IAT 2003), 13-17 October 2003, Halifax, Canada, pp. 275-281, 2003, IEEE Computer Society, 0-7695-1931-8. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
34 | Paolo Traverso, Piergiorgio Bertoli |
Mechanized result verification: an industrial application. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 3(1), pp. 78-92, 2000. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AGTIVE ![In: Applications of Graph Transformations with Industrial Relevance, International Workshop, AGTIVE'99, Kerkrade, The Netherlands, September 1-3, 1999, Proceedings, pp. 271-278, 1999, Springer, 3-540-67658-9. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
33 | Sa'ed Abed, Otmane Aït Mohamed |
MDGs Reduction Technique Based on the HOL Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMVL ![In: 40th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2010, Barcelona, Spain, 26-28 May 2010, pp. 15-20, 2010, IEEE Computer Society, 978-0-7695-4024-5. The full citation details ...](Pics/full.jpeg) |
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) ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, pp. 13-18, 1991, IEEE Computer Society, 0-8186-2445-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
UTP ![In: Unifying Theories of Programming, First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006, Revised Selected Papers, pp. 123-140, 2006, Springer, 3-540-34750-X. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Unifying Theories of Programming, theorem prover |
31 | Mizuhito Ogawa, Eiichi Horita, Satoshi Ono |
Proving Properties of Incremental Merkle Trees. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, pp. 424-440, 2005, Springer, 3-540-28005-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFM ![In: Integrated Formal Methods, 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005, Proceedings, pp. 246-265, 2005, Springer, 3-540-30492-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASE ![In: 1997 International Conference on Automated Software Engineering, ASE 1997, Lake Tahoe, CA, USA, November 2-5, 1997, pp. 246-254, 1997, IEEE Computer Society, 0-8186-7961-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, pp. 71-88, 2020, Springer, 978-3-030-53517-9. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
30 | Mihir Parang Mehta |
Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018., pp. 18-29, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
30 | Shuling Wang, Naijun Zhan, Liang Zou |
An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings, pp. 382-399, 2015, Springer, 978-3-319-25422-7. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
30 | Gábor Tardos |
Multi-prover Encoding Schemes and Three-prover Proof Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Comput. Syst. Sci. ![In: J. Comput. Syst. Sci. 53(2), pp. 251-260, 1996. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
30 | Gábor Tardos |
Multi-Prover Encoding Schemes and Three-Prover Proof Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SCT ![In: Proceedings of the Ninth Annual Structure in Complexity Theory Conference, Amsterdam, The Netherlands, June 28 - July 1, 1994, pp. 308-317, 1994, IEEE Computer Society, 0-8186-5670-0. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
30 | Aleksandar Krapez, Miodrag Kapetanovic, Zoran Ognjanovic, Tatjana Petrovic |
Prover 91 - A Parallel Theorem Prover (Extended Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Workshop Theorem Proving with Analytic Tableaux and Related Methods, Lautenbach. Universität Karlsruhe, Fakultät für Informatik, Institut für Logik, Komplexität und Deduktionssysteme, Interner Bericht 8/92, March 18-20, 1992, pp. 43-45, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
30 | Steven Greenbaum, David A. Plaisted |
The Illinois Prover: A General Purpose Resolution Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings, pp. 685-687, 1986, Springer, 3-540-16780-3. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP DOI BibTeX RDF |
|
30 | Shang-Ching Chou |
GEO-Prover - A Geometry Theorem Prover Developed at UT. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings, pp. 679-680, 1986, Springer, 3-540-16780-3. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP DOI BibTeX RDF |
|
29 | Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
Dei: A Theorem Prover for Terms with Integer Exponents. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, pp. 146-150, 2009, Springer, 978-3-642-02958-5. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
29 | Dru McCandless, Leo Obrst, Shayn Hawthorne |
Dynamic Web Service Assembly Using OWL and a Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICSC ![In: Proceedings of the 3rd IEEE International Conference on Semantic Computing (ICSC 2009), 14-16 September 2009, Berkeley, CA, USA, pp. 336-341, 2009, IEEE Computer Society, 978-0-7695-3800-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, pp. 309-313, 2008, Springer, 978-3-540-70543-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
29 | André Platzer, Jan-David Quesel |
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description). ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, pp. 171-178, 2008, Springer, 978-3-540-71069-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, pp. 413-427, 2008, Springer, 978-3-540-78799-0. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
29 | Aaron Richard Coble |
Formalized Information-Theoretic Proofs of Privacy Using the HOL4 Theorem-Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Privacy Enhancing Technologies ![In: Privacy Enhancing Technologies, 8th International Symposium, PETS 2008, Leuven, Belgium, July 23-25, 2008, Proceedings, pp. 77-98, 2008, Springer, 978-3-540-70629-8. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
29 | Laura I. Meikle, Jacques D. Fleuriot |
Combining Isabelle and QEPCAD-B in the Prover's Palette. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISC/MKM/Calculemus ![In: Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings, pp. 315-330, 2008, Springer, 978-3-540-85109-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
29 | Richard Bonichon, David Delahaye, Damien Doligez |
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, pp. 151-165, 2007, Springer, 978-3-540-75558-6. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
29 | Behzad Akbarpour, Lawrence C. Paulson |
Extending a Resolution Prover for Inequalities on Elementary Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, pp. 47-61, 2007, Springer, 978-3-540-75558-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICDE ![In: Proceedings of the 23rd International Conference on Data Engineering, ICDE 2007, The Marmara Hotel, Istanbul, Turkey, April 15-20, 2007, pp. 1521-1522, 2007, IEEE Computer Society, 1-4244-0802-4. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 135-150, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM ![In: FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings, pp. 64-80, 2006, Springer, 3-540-37215-6. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
29 | Tadashi Takahashi, Hidetsune Kobayashi |
The Effect of the Theorem Prover in Cognitive Science. ![Search on Bibsonomy](Pics/bibsonomy.png) |
International Conference on Computational Science (1) ![In: Computational Science - ICCS 2006, 6th International Conference, Reading, UK, May 28-31, 2006, Proceedings, Part I, pp. 924-927, 2006, Springer, 3-540-34379-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
29 | Giuseppe Persiano, Ivan Visconti |
Single-Prover Concurrent Zero Knowledge in Almost Constant Rounds. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALP ![In: Automata, Languages and Programming, 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings, pp. 228-240, 2005, Springer, 3-540-27580-0. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
29 | Kaustuv Chaudhuri, Frank Pfenning |
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, pp. 69-83, 2005, Springer, 3-540-28005-7. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
29 | Andreas Abel 0001, Thierry Coquand, Ulf Norell |
Connecting a Logical Framework to a First-Order Logic Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FroCoS ![In: Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, Proceedings, pp. 285-301, 2005, Springer, 3-540-29051-6. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
29 | Kenneth L. McMillan |
An Interpolating Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, pp. 16-30, 2004, Springer, 3-540-21299-X. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
29 | Nicola Olivetti, Gian Luca Pozzato |
CondLean: A Theorem Prover for Conditional Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2003, Rome, Italy, September 9-12, 2003. Proceedings, pp. 264-270, 2003, Springer, 3-540-40787-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, pp. 670-684, 2001, Springer, 3-540-42254-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
29 | Jens Happe |
The MODPROF Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, pp. 459-463, 2001, Springer, 3-540-42254-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
29 | David Spelt, Susan Even |
A Theorem Prover-Based Analysis Tool for Object-Oriented Databases. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS '99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings, pp. 375-389, 1999, Springer, 3-540-65703-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, pp. 39-44, 1998, Springer, 3-540-64608-6. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
29 | Michel Levy |
Prover KT4. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX '98, Oisterwijk, The Netherlands, May 5-8, 1998, Proceedings, pp. 31-32, 1998, Springer, 3-540-64406-7. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
29 | Yves Ledru |
Identifying Pre-Conditions with the Z/EVES Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASE ![In: The Thirteenth IEEE Conference on Automated Software Engineering, ASE 1998, Honolulu, Hawaii, USA, October 13-16, 1998, pp. 32-, 1998, IEEE Computer Society, 0-8186-8750-9. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
29 | Maria Paola Bonacina |
The Clause-Diffusion Theorem Prover Peers-mcd (System Description). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, pp. 53-56, 1997, Springer, 3-540-63104-6. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
29 | Scott Hazelhurst, Carl-Johan H. Seger |
A simple theorem prover based on symbolic trajectory evaluation and BDD's. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. ![In: IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 14(4), pp. 413-422, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
29 | Peter Baumgartner 0001, Ulrich Furbach |
PROTEIN: A PROver with a Theory Extension INterface. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings, pp. 769-773, 1994, Springer, 3-540-58156-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
29 | Maria Paola Bonacina, Jieh Hsiang |
Distributed Deduction by Clause-Diffusion: The Aquarius Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DISCO ![In: Design and Implementation of Symbolic Computation Systems, International Symposium, DISCO '93, Gmunden, Austria, September 15-17, 1993, Proceedings, pp. 272-287, 1993, Springer, 3-540-57235-X. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
29 | Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita 0002 |
MGTP: A Parallel Theorem Prover Based on Lazy Model Generation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, pp. 776-780, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
29 | Aline Deruyver |
EMMY: A Refutational Theorem Prover for First-Order Logic with Equation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, pp. 439-441, 1991, Springer, 3-540-53904-2. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
29 | Dror Lapidot, Adi Shamir |
A One-Round, Two-Prover, Zero-Knowledge Protocol for NP. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CRYPTO ![In: Advances in Cryptology - CRYPTO '91, 11th Annual International Cryptology Conference, Santa Barbara, California, USA, August 11-15, 1991, Proceedings, pp. 213-224, 1991, Springer, 3-540-55188-3. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
29 | Larry M. Hines |
Str+ve-Subset: The Str+ve-based Subset Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 193-206, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
29 | Mark Tarver |
An Examination of the Prolog Technology Theorem-Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 322-335, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
PTTP, metalevel reasoning, Prolog Normal Form, refinement |
29 | Johann Schumann, Reinhold Letz |
PARTHEO: A High-Performance Parallel Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 40-56, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CRYPTO ![In: Advances in Cryptology - CRYPTO '90, 10th Annual International Cryptology Conference, Santa Barbara, California, USA, August 11-15, 1990, Proceedings, pp. 366-377, 1990, Springer, 3-540-54508-5. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
29 | Heikki Tuominen |
Proving Properties of Elementary Net Systems with a Special-Purpose Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automatic Verification Methods for Finite State Systems ![In: Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings, pp. 97-104, 1989, Springer, 3-540-52148-8. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
29 | Michael Ben-Or, Shafi Goldwasser, Joe Kilian, Avi Wigderson |
Efficient Identification Schemes Using Two Prover Interactive Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CRYPTO ![In: Advances in Cryptology - CRYPTO '89, 9th Annual International Cryptology Conference, Santa Barbara, California, USA, August 20-24, 1989, Proceedings, pp. 498-506, 1989, Springer, 3-540-97317-6. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
29 | Mark E. Stickel |
A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings, pp. 573-587, 1986, Springer, 3-540-16780-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings, pp. 154-169, 1980, Springer, 3-540-10009-1. The full citation details ...](Pics/full.jpeg) |
1980 |
DBLP DOI BibTeX RDF |
|
Displaying result #1 - #100 of 2141 (100 per page; Change: ) Pages: [ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ >>] |
|