Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
23 | Gordon Stewart 0001, Lennart Beringer, Andrew W. Appel |
Verified heap theorem prover by paramodulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012, pp. 3-14, 2012, ACM, 978-1-4503-1054-3. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
23 | Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois |
Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, pp. 332-338, 2012, Springer, 978-3-642-31364-6. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
23 | Hao Xu 0011 |
How To Efficiently Implement An OSHL-Based Automatic Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2012 |
DOI RDF |
|
23 | Erik Zawadzki, Geoffrey J. Gordon, André Platzer |
An Instantiation-Based Theorem Prover for First-Order Programming. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISTATS ![In: Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, AISTATS 2011, Fort Lauderdale, USA, April 11-13, 2011, pp. 855-863, 2011, JMLR.org. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP BibTeX RDF |
|
23 | Ángel Mora 0001, Emilio Muñoz-Velasco, Joanna Golinska-Pilarek |
Implementing a relational theorem prover for modal logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Comput. Math. ![In: Int. J. Comput. Math. 88(9), pp. 1869-1884, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Tjark Weber |
SMT solvers: new oracles for the HOL theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 13(5), pp. 419-429, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | David S. Hardin, Julien Schmaltz (eds.) |
Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Jussi Rintanen |
Constructing Conditional Plans by a Theorem-Prover ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1105.5465, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP BibTeX RDF |
|
23 | Ralph-Johan Back, Johannes Eriksson |
An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu ![In: Proceedings First Workshop on CTP Components for Educational Software, THedu'11, Wroclaw, Poland, 31th July 2011., pp. 29-48, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Osman Hasan, Sofiène Tahar |
Reasoning about conditional probabilities in a higher-order-logic theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Appl. Log. ![In: J. Appl. Log. 9(1), pp. 23-40, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Krystof Hoder, Laura Kovács, Andrei Voronkov |
Case Studies on Invariant Generation Using a Saturation Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MICAI (1) ![In: Advances in Artificial Intelligence - 10th Mexican International Conference on Artificial Intelligence, MICAI 2011, Puebla, Mexico, November 26 - December 4, 2011, Proceedings, Part I, pp. 1-15, 2011, Springer, 978-3-642-25323-2. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi |
The Matita Interactive Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, pp. 64-69, 2011, Springer, 978-3-642-22437-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Juan Antonio Navarro Pérez, Andrey Rybalchenko |
Separation logic + superposition calculus = heap theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLDI ![In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pp. 556-566, 2011, ACM, 978-1-4503-0663-8. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Régis Alenda, Nicola Olivetti |
CSymLean: A Theorem Prover for the Logic CSL over Symmetric Minspaces. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011. Proceedings, pp. 21-26, 2011, Springer, 978-3-642-22118-7. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Magnus O. Myreen, Jared Davis |
A Verified Runtime for a Verified Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, pp. 265-280, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Simon Foster 0001, Georg Struth |
Integrating an Automated Theorem Prover into Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NASA Formal Methods ![In: NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, pp. 116-130, 2011, Springer, 978-3-642-20397-8. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Harsh Raju Chamarthi, Panagiotis Manolios |
Automated specification analysis using an interactive theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: International Conference on Formal Methods in Computer-Aided Design, FMCAD '11, Austin, TX, USA, October 30 - November 02, 2011, pp. 46-53, 2011, FMCAD Inc., 978-0-9835678-1-3. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP BibTeX RDF |
|
23 | Andrea Asperti, Maria Emilia Maietti, Claudio Sacerdoti Coen, Giovanni Sambin, Silvio Valentini |
Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings, pp. 278-280, 2011, Springer, 978-3-642-22672-4. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Freek Verbeek, Julien Schmaltz |
Formal verification of a deadlock detection algorithm ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 103-112, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Peter Reid, Ruben Gamboa |
Implementing an Automatic Differentiator in ACL2 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 61-69, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Sol Swords, Jared Davis |
Bit-Blasting ACL2 Theorems ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 84-102, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Matt Kaufmann, J Strother Moore |
How Can I Do That with ACL2? Recent Enhancements to ACL2 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 46-60, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Peter-Michael Seidel |
Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 70-83, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Mike Dahlin, Ryan Johnson 0003, Robert Bellarmine Krug, Michael McCoyd, William D. Young |
Toward the Verification of a Simple Hypervisor ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 28-45, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | John R. Cowles, Ruben Gamboa |
Verifying Sierpinski and Riesel Numbers in ACL2 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 20-27, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios |
Integrating Testing and Interactive Theorem Proving ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011., pp. 4-19, 2011. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
23 | Scott Uk-Jin Lee, Gillian Dobbie, Jing Sun 0002, Lindsay Groves |
Theorem prover approach to semistructured data design. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 37(1), pp. 1-60, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
23 | Gang Chen |
Formalization of a Parameterized Parallel Adder Within the Coq Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. ![In: IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(1), pp. 149-153, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
23 | Tim vor der Brück, Hermann Helbig |
Meronymy Extraction Using An Automated Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Lang. Technol. Comput. Linguistics ![In: J. Lang. Technol. Comput. Linguistics 25(1), pp. 57-81, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP BibTeX RDF |
|
23 | Behzad Akbarpour, Lawrence C. Paulson |
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 44(3), pp. 175-205, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
23 | Sana Stojanovic, Vesna Pavlovic, Predrag Janicic |
A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry - 8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Selected Papers, pp. 201-220, 2010, Springer, 978-3-642-25069-9. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
23 | Andrew Butterfield |
Saoithín: A Theorem Prover for UTP. ![Search on Bibsonomy](Pics/bibsonomy.png) |
UTP ![In: Unifying Theories of Programming - Third International Symposium, UTP 2010, Shanghai, China, November 15-16, 2010. Proceedings, pp. 137-156, 2010, Springer, 978-3-642-16689-1. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
23 | Tim vor der Brück, Holger Stenzhorn |
Logical Ontology Validation Using an Automatic Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ECAI ![In: ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings, pp. 491-496, 2010, IOS Press, 978-1-60750-605-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
23 | Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine |
GridTPT: a distributed platform for Theorem Prover Testing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PAAR@IJCAR ![In: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Scotland, UK, July 14, 2010, pp. 33-39, 2010, EasyChair. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
23 | Konstantin Korovin, Christoph Sticksel |
iProver-Eq: An Instantiation-Based Theorem Prover with Equality. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, pp. 196-202, 2010, Springer, 978-3-642-14202-4. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
23 | Dominic Richards, David R. Lester |
A Prototype Embedding of Bluespec SystemVerilog in the PVS Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NASA Formal Methods ![In: Second NASA Formal Methods Symposium - NFM 2010, Washington D.C., USA, April 13-15, 2010. Proceedings, pp. 139-148, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP BibTeX RDF |
|
23 | Maksym Bortin |
An approach to the extension of a theorem prover by advanced structuring mechanisms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2010 |
RDF |
|
23 | Régis Alenda, Nicola Olivetti, Gian Luca Pozzato |
CSL-lean: A Theorem-prover for the Logic of Comparative Concept Similarity. ![Search on Bibsonomy](Pics/bibsonomy.png) |
M4M ![In: Proceedings of the 6th Workshop on Methods for Modalities, M4M-6 2009, Copenhagen, Denmark, November 12-14, 2009, pp. 3-16, 2009, Elsevier. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
23 | Ricky W. Butler |
Formalization of the Integral Calculus in the PVS Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Formaliz. Reason. ![In: J. Formaliz. Reason. 2(1), pp. 1-26, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
23 | 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 |
|
23 | Shimmi Asokan, G. Santhosh Kumar, N. Jaya Lal |
Modeling of ALFA Programs Using PVS Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ARTCom ![In: ARTCom 2009, International Conference on Advances in Recent Technologies in Communication and Computing, Kottayam, Kerala, India, 27-28 October 2009, pp. 373-375, 2009, IEEE Computer Society, 978-0-7695-3845-7. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
23 | Laura Kovács, Andrei Voronkov |
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SYNASC ![In: 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2009, Timisoara, Romania, September 26-29, 2009, pp. 10, 2009, IEEE Computer Society, 978-1-4244-5910-0. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
23 | Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov |
Verifying equivalence of memories using a first order logic theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA, pp. 128-135, 2009, IEEE, 978-1-4244-4966-8. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
23 | John Byrnes, Michael Buchanan, Michael Ernst, Philip Miller, Chris Roberts, Robert Keller |
Visualizing Proof Search for Theorem Prover Development. ![Search on Bibsonomy](Pics/bibsonomy.png) |
UITP@TPHOLs ![In: Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, UITP@TPHOLs 2008, Montréal, Canada, August 22, 2008, pp. 23-38, 2008, Elsevier. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
23 | Andrew Gacek |
The Abella Interactive Theorem Prover (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. 154-161, 2008, Springer, 978-3-540-71069-1. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
23 | Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane |
The Performance of Combining Multiway Decision Graphs and HOL Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FDL ![In: Forum on specification and Design Languages, FDL 2008, September 23-25, 2008, Stuttgart, Germany, Proceedings, pp. 136-141, 2008, IEEE, 978-1-4244-2265-4. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
23 | Patrick Barlatier, Richard Dapoigny |
A Theorem Prover with Dependent Types for Reasoning about Actions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STAIRS ![In: STAIRS 2008 - Proceedings of the Fourth Starting AI Researchers' Symposium, Patras, Greece, 21-25 July, 2008, pp. 12-23, 2008, IOS Press, 978-1-58603-893-9. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
23 | Bo Guo, Mahadevan Subramaniam |
Formal Change Impact Analyses of Extended Finite State Machines Using a Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEFM ![In: Sixth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008, Cape Town, South Africa, 10-14 November 2008, pp. 335-344, 2008, IEEE Computer Society, 978-0-7695-3437-4. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
23 | Marco Cadoli, Toni Mancini |
Using a Theorem Prover for Reasoning on Constraint Problems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Appl. Artif. Intell. ![In: Appl. Artif. Intell. 21(4&5), pp. 383-404, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
23 | Jolyon Clulow |
Robbing the Bank with a Theorem Prover - (Transcript of Discussion). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Security Protocols Workshop ![In: Security Protocols - 15th International Workshop, Brno, Czech Republic, April 18-20, 2007. Revised Selected Papers, pp. 172-177, 2007, Springer, 978-3-642-17772-9. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
23 | Paul Youn, Ben Adida, Mike Bond, Jolyon Clulow, Jonathan Herzog, Amerson Lin, Ronald L. Rivest, Ross J. Anderson |
Robbing the Bank with a Theorem Prover - (Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Security Protocols Workshop ![In: Security Protocols - 15th International Workshop, Brno, Czech Republic, April 18-20, 2007. Revised Selected Papers, pp. 171, 2007, Springer, 978-3-642-17772-9. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
23 | Ralph Butler, Chrisila C. Pettey |
A Bilingual Theorem Prover for Evaluating HPC Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PDPTA ![In: Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2007, Las Vegas, Nevada, USA, June 25-28, 2007, Volume 2, pp. 1000-1003, 2007, CSREA Press, 1-60132-021-3. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP BibTeX RDF |
|
23 | Cezary Kaliszyk, Freek Wiedijk |
Certified Computer Algebra on Top of an Interactive Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings, pp. 94-105, 2007, Springer, 978-3-540-73083-5. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
23 | Louise A. Dennis |
Enhancing Theorem Prover Interfaces with Program Slice Information. ![Search on Bibsonomy](Pics/bibsonomy.png) |
UITP@FLoC ![In: Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, UITP@FLoC 2006, Seattle, WA, USA, August 21, 2006, pp. 19-33, 2006, Elsevier. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
23 | Kamal Aboul-Hosn, Dexter Kozen |
KAT-ML: an interactive theorem prover for Kleene algebra with tests. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Appl. Non Class. Logics ![In: J. Appl. Non Class. Logics 16(1-2), pp. 9-34, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
23 | Panagiotis Manolios, Matthew Wilding (eds.) |
Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006 ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![ACM, 0-9788493-0-2 The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP BibTeX RDF |
|
23 | Anduo Wang, Fei He 0001, Ming Gu 0001, Xiaoyu Song |
Verifying Java Programs By Theorem Prover HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
COMPSAC (1) ![In: 30th Annual International Computer Software and Applications Conference, COMPSAC 2006, Chicago, Illinois, USA, September 17-21, 2006. Volume 1, pp. 139-142, 2006, IEEE Computer Society, 0-7695-2655-1. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
23 | David L. Rager |
Adding parallelism capabilities to ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 90-94, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
pand, parallel ACL2, pcall, plet, por, granularity, functional language |
23 | Jared Davis |
Memories: array-like records for ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 57-60, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
MBE, fixnum optimization, linear address spaces, arrays, records, ACL2 |
23 | John R. Cowles, Ruben Gamboa |
Unique factorization in ACL2: Euclidean domains. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 21-27, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Boyer-Moore logic, Euclidean domains, unique factorization, ACL2 |
23 | Matt Kaufmann, J Strother Moore |
Double rewriting for equivalential reasoning in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 103-106, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
double-rewrite, verification, formal methods, rewriting, congruences, equivalence relations |
23 | Ruben Gamboa, John R. Cowles |
Implementing a cost-aware evaluator for ACL2 expressions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 71-80, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
ACL2 evaluator, function cost, evaluators |
23 | Jared Davis |
Reasoning about ACL2 file input. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 117-126, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
UTF-8, file input, ACL2, unicode, exhaustive testing |
23 | Sandip Ray |
Quantification in tail-recursive function definitions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 95-98, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
formal methods, logic, ACL2, conservativity, skolemization |
23 | Sol Swords, William R. Cook |
Soundness of the simply typed lambda calculus in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 35-39, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
lambda-calculus, soundness, ACL2 |
23 | Robert S. Boyer, Warren A. Hunt Jr. |
Function memoization and unique object representation for ACL2 functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 81-89, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
ACL2 workshop, function memoization, hash CONS, hash CONSing, Lisp, ACL2 |
23 | Tony Hoare |
The ideal of verified software. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 61-62, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
23 | David A. Greve |
Parameterized congruences in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 28-34, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
23 | Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds |
An embedding of the ACL2 logic in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 40-46, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
HOL4, proof oracle, sound translation, verification, formal methods, logic, first-order logic, higher-order logic, ACL2, HOL |
23 | Warren A. Hunt Jr., Erik Reeber |
A SAT-based procedure for verifying finite state machines in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 127-135, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
satisfiability solving, theorem proving, hardware verification, ACL2 |
23 | Lee Pike, Mark Shields, John Matthews |
A verifying core for a cryptographic language compiler. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 1-10, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
cryptography, certification, optimizing compiler, ACL2, high-assurance, certifying compiler, verifying compiler |
23 | Warren A. Hunt Jr., Serita M. Nelesen |
Phylogenetic trees in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 99-102, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
ACL2, phylogenetics |
23 | David S. Hardin, Eric W. Smith, William D. Young |
A robust machine code proof framework for highly secure applications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACL2 ![In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 11-20, 2006, ACM, 0-9788493-0-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
cryptography, theorem proving, certification, symbolic simulation, ACL2, high-assurance, processor modeling |
23 | Tjark Weber |
Integrating a SAT Solver with an LCF-style Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PDPAR@CAV ![In: Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, PDPAR@CAV 2005, Edinburgh, UK, July 12, 2005, pp. 67-78, 2005, Elsevier. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
23 | David Déharbe, Silvio Ranise, Jorgiano Vidal |
Distributing the Workload in a Lazy Theorem-Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBMF ![In: Proceedings of the Second Brazilian Symposium on Formal Methods, SBMF 2005, Porto Alegre, RS, Brazil, November 30, 2005, pp. 21-37, 2005, Elsevier. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
23 | Kenneth L. McMillan |
An interpolating theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 345(1), pp. 101-121, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
23 | David Detlefs, Greg Nelson, James B. Saxe |
Simplify: a theorem prover for program checking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 52(3), pp. 365-473, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
Theorem proving, decision procedures, program checking |
23 | Tom Ridge, James Margetson |
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 294-309, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
23 | K. Rustan M. Leino, Madan Musuvathi, Xinming Ou |
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. ![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. 334-348, 2005, Springer, 3-540-25333-5. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
23 | Marco Cadoli, Toni Mancini |
Using a Theorem Prover for Reasoning on Constraint Problems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI*IA ![In: AI*IA 2005: Advances in Artificial Intelligence, 9th Congress of the Italian Association for Artificial Intelligence, Milan, Italy, September 21-23, 2005, Proceedings, pp. 38-49, 2005, Springer, 3-540-29041-9. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
23 | Choon Kyu Kim |
Exploiting parallelism: highly competitive semantic tree theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Comput. Math. ![In: Int. J. Comput. Math. 81(9), pp. 1051-1067, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
23 | Nicola Olivetti, Gian Luca Pozzato, Camilla Schwind |
A Sequent Calculus and a Theorem Prover for Standard Conditional Logics ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR cs.LO/0407064, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP BibTeX RDF |
|
23 | Peter Kullmann, Sandra A. Sandri |
An annotated logic theorem prover for an extended possibilistic logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Fuzzy Sets Syst. ![In: Fuzzy Sets Syst. 144(1), pp. 67-91, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
23 | Tom Ridge |
A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2004, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP BibTeX RDF |
|
23 | Yasuyuki Shirai, Ryuzo Hasegawa |
Answer Set Computation Based on a Minimal Model Generation Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PRICAI ![In: PRICAI 2004: Trends in Artificial Intelligence, 8th Pacific Rim International Conference on Artificial Intelligence, Auckland, New Zealand, August 9-13, 2004, Proceedings, pp. 43-52, 2004, Springer, 3-540-22817-9. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
23 | Arnold Binas, John K. Slaney |
Semantically Guiding a First-Order Theorem Prover with a Soft Model. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AAAI ![In: Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, July 25-29, 2004, San Jose, California, USA, pp. 948-949, 2004, AAAI Press / The MIT Press, 0-262-51183-5. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP BibTeX RDF |
|
23 | John K. Slaney, Arnold Binas, David Price |
Guiding a Theorem Prover with Soft Constraints. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ECAI ![In: Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI'2004, including Prestigious Applicants of Intelligent Systems, PAIS 2004, Valencia, Spain, August 22-27, 2004, pp. 221-225, 2004, IOS Press, 1-58603-452-9. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP BibTeX RDF |
|
23 | Daniel Winterstein |
Dr.Doodle: A Diagrammatic Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR Doctoral Programme ![In: Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning, Cork, Ireland, July 4-8, 2004., 2004, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP BibTeX RDF |
|
23 | Zhen Li |
An implementation of a tableau theorem prover for modal logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR Doctoral Programme ![In: Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning, Cork, Ireland, July 4-8, 2004., 2004, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP BibTeX RDF |
|
23 | Thomas Hillenbrand |
Citius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FTP ![In: 4th International Workshop on First-Order Theorem Proving, FTP 2003, in connection with RDP 2003, Federated Conference on Rewriting, Deduction and Programming, Valencia, Spain, June 12-14, 2003, pp. 9-21, 2003, Elsevier. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
23 | Choon Kyu Kim, Monty Newborn |
Competitive Semantic Tree Theorem Prover with Resolutions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PVM/MPI ![In: Recent Advances in Parallel Virtual Machine and Message Passing Interface,10th European PVM/MPI Users' Group Meeting, Venice, Italy, September 29 - October 2, 2003, Proceedings, pp. 227-231, 2003, Springer, 3-540-20149-1. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
23 | Stephan Schulz 0001 |
E - a brainiac theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI Commun. ![In: AI Commun. 15(2-3), pp. 111-126, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP BibTeX RDF |
|
23 | Kahlil Hodgson, John K. Slaney |
TPTP, CASC and the development of a semantically guided theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI Commun. ![In: AI Commun. 15(2-3), pp. 135-146, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP BibTeX RDF |
|
23 | Dominique Pastre |
Strong and weak points of the MUSCADET theorem prover - examples from CASC-JC. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI Commun. ![In: AI Commun. 15(2-3), pp. 147-160, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP BibTeX RDF |
|
23 | Paul Z. Kolano |
Proof assistance for real-time systems using an interactive theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 282(1), pp. 53-99, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
23 | Orieta Celiku, Joakim von Wright |
Theorem Prover Support for Precondition and Correctness Calculation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering, 4th International Conference on Formal Engineering Methods, ICFEM 2002 Shanghai, China, October 21-25, 2002, Proceedings, pp. 299-310, 2002, Springer, 3-540-00029-1. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
23 | Jamie Shield, Ian J. Hayes, David A. Carrington |
Using Theory Interpretation to Mechanise the Reals in a Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CATS ![In: Computing: The Australasian Theory Symposium, CATS 2001, Gold Coast, Australia, January 29-30, 2001, pp. 266-281, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
23 | Ortrun Ibens, Marc Fuchs |
An Automated Theorem Prover Based on Connection Tableau Calculi with Disjunctive Constraints. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Artif. Intell. Tools ![In: Int. J. Artif. Intell. Tools 10(1-2), pp. 181-198, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
23 | M. Randall Holmes, Jim Alves-Foss |
The Watson Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 26(4), pp. 357-408, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
23 | Chih-Hung Wu, Shie-Jue Lee |
Parallelization of a Hyper-Linking-Based Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 26(1), pp. 67-106, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|