Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
23 | Alessandro Avellone, Marco Benini, Ugo Moscato |
How to Avoid the Formal Verification of a Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Log. J. IGPL ![In: Log. J. IGPL 9(1), pp. 1-25, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
23 | Yves Bertot |
Formalizing a JVML Verifier for Initialization in a Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings, pp. 14-24, 2001, Springer, 3-540-42345-1. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
23 | Iara Moema Oberg Vilela, Priscila Machado Vieira Lima |
Conjecturing the Cognitive Plausibility of an ANN Theorem-Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IWANN (1) ![In: Connectionist Models of Neurons, Learning Processes and Artificial Intelligence, 6th International Work-Conference on Artificial and Natural Neural Networks, IWANN 2001 Granada, Spain, June 13-15, 2001, Proceedings, Part I, pp. 822-830, 2001, Springer, 3-540-42235-8. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
23 | Vanderlei Moraes Rodrigues, Dominique Borrione, Philippe Georgelin |
Using the ACL2 Theorem Prover to Reason about VHDL Components. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RITA ![In: RITA 7(1), pp. 129-148, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP BibTeX RDF |
|
23 | Hiroshi Sakai, Akimichi Okuma |
On a Theorem Prover for Variational Logic Programs with Functors Setu and Sets. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Uncertain. Fuzziness Knowl. Based Syst. ![In: Int. J. Uncertain. Fuzziness Knowl. Based Syst. 8(1), pp. 73-92, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
23 | Lila Rao, Han Reichgelt |
STIRDAT: A system tightly integrating relational databases and a theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Data Knowl. Eng. ![In: Data Knowl. Eng. 34(1), pp. 1-20, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
23 | Dirk Fuchs |
Cooperation in heterogeneous theorem prover networks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2000 |
RDF |
|
23 | Ulrich Kühler |
A tactic-based inductive theorem prover for data types with partial operations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2000 |
RDF |
|
23 | Joachim Draeger |
Redundancy-Free Lemmatization in the Automated Model-Elimination Theorem Prover AI-SETHEO. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings, pp. 431-435, 2000, Springer, 3-540-67697-X. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
23 | Gernot Stenz, Andreas Wolf 0005 |
E-SETHEO: An Automated3 Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings, pp. 436-440, 2000, Springer, 3-540-67697-X. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
23 | Ivan I. Garibay |
Generating Text with a Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ANLP ![In: 6th Applied Natural Language Processing Conference, ANLP 2000, Seattle, Washington, USA, April 29 - May 4, 2000, pp. 13-18, 2000, ACL. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP BibTeX RDF |
|
23 | Allen Van Gelder, Fumiaki Okushi |
A propositional theorem prover to solve planning and other problems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Ann. Math. Artif. Intell. ![In: Ann. Math. Artif. Intell. 26(1-4), pp. 87-112, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
23 | Jussi Rintanen |
Constructing Conditional Plans by a Theorem-Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Artif. Intell. Res. ![In: J. Artif. Intell. Res. 10, pp. 323-352, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
23 | Joseph A. Goguen |
Social and Semiotic Analyses for Theorem Prover User Interface Design 1. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 11(3), pp. 272-301, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
Algebraic semiotics, CSCW, User interface design, Theorem proving, Algebraic specification, Semiotics, Sociology, Narratology |
23 | José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos |
Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APPIA-GULP-PRODE ![In: 1999 Joint Conference on Declarative Programming, AGP'99, L'Aquila, Italy, September 6-9, 1999, pp. 289-304, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP BibTeX RDF |
|
23 | Jean-Michel Richer, Jean-Jacques Chabrier |
Sacre: a Constraint Satisfaction Problem Based Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AAAI/IAAI ![In: Proceedings of the Sixteenth National Conference on Artificial Intelligence and Eleventh Conference on Innovative Applications of Artificial Intelligence, July 18-22, 1999, Orlando, Florida, USA., pp. 306-311, 1999, AAAI Press / The MIT Press, 0-262-51106-1. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP BibTeX RDF |
|
23 | Andrei Voronkov |
KK: a theorem prover for K. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, pp. 383-387, 1999, Springer, 3-540-66222-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
23 | Dieter Hutter, Alan Bundy |
The Design of the CADE-16 Inductive Theorem Prover Contest. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, pp. 374-377, 1999, Springer, 3-540-66222-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
23 | Ulrich Endriss |
A Time Efficient KE Based Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX '99, Saratoga Springs, NY, USA, June 7-11, 1999, Proceedings, pp. 313-318, 1999, Springer, 3-540-66086-0. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
23 | Alvaro Kilkerry Neto, Gerson Zaverucha, Luís Alfredo Vidal de Carvalho |
An implementation of a theorem prover in symmetric neural networks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCNN ![In: International Joint Conference Neural Networks, IJCNN 1999, Washington, DC, USA, July 10-16, 1999, pp. 4139-4144, 1999, IEEE. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
23 | Robert F. Stärk |
The Theoretical Foundations of LPTP (A Logic Program Theorem Prover). ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Log. Program. ![In: J. Log. Program. 36(3), pp. 241-269, 1998. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
23 | Tristan Cazenave |
Synthesis of an Efficient Tactical Theorem Prover for the Game of Go. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Comput. Surv. ![In: ACM Comput. Surv. 30(3es), pp. 18, 1998. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
23 | Peter Jakobi, Andreas Wolf |
DBFW: A Simple DataBase FrameWork for the Evaluation and Maintenance of Automated Theorem Prover Data. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSMR ![In: 2nd Euromicro Conference on Software Maintenance and Reengineering (CSMR '98), 8-11 March 1998, Florence, Italy, pp. 185-188, 1998, IEEE Computer Society, 0-8186-8421-6. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
23 | Christoph Benzmüller, Michael Kohlhase |
System Description: LEO - A Higher-Order Theorem Prover. ![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. 139-144, 1998, Springer, 3-540-64675-2. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
23 | Matt Kaufmann, J Strother Moore |
An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 23(4), pp. 203-213, 1997. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
total functions, microcode verification, floating point division, Formal verification, digital signal processing, type checking, computational logic, automatic theorem proving, partial functions |
23 | M. Paramasivam, David A. Plaisted |
RRTP - A Replacement Rule Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 18(2), pp. 221-226, 1997. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
23 | Christian B. Suttner |
SPTHEO - A Parallel Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 18(2), pp. 253-258, 1997. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
23 | Heng Chu, David A. Plaisted |
CLIN-S - A Semantically Guided First-Order Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 18(2), pp. 183-188, 1997. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
23 | Thomas Kolbe, Sabine Glesner |
Many-Sorted Logic in a Learning Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
KI ![In: KI-97: Advances in Artificial Intelligence, 21st Annual German Conference on Artificial Intelligence, Freiburg, Germany, September 9-12, 1997, Proceedings, pp. 75-86, 1997, Springer, 3-540-63493-2. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
23 | Thomas R. Ioerger |
Integrating a Spatial Reasoner with a Resolution Theorem-Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AAAI/IAAI ![In: Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, July 27-31, 1997, Providence, Rhode Island, USA., pp. 145-152, 1997, AAAI Press / The MIT Press, 0-262-51095-2. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP BibTeX RDF |
|
23 | Ryuzo Hasegawa, Hiroshi Fujita 0002, Miyuki Koshimura |
MGTP: A Model Generation Theorem Prover - Its Advanced Features and Applications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX '97, Pont-à-Mousson, France, May 13-16, 1997, Proceedings, pp. 1-15, 1997, Springer, 3-540-62920-3. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
23 | Jens Otten |
ileanTAP: An Intuitionistic Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX '97, Pont-à-Mousson, France, May 13-16, 1997, Proceedings, pp. 307-312, 1997, Springer, 3-540-62920-3. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
23 | Robert Sandner, Olaf Müller |
Theorem Prover Support for the Refinement of Stream Processing Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS '97, Enschede, The Netherlands, April 2-4, 1997, Proceedings, pp. 351-365, 1997, Springer, 3-540-62790-1. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
23 | Christian B. Suttner |
SPTHEO - A PVM-Based Parallel Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PVM ![In: Parallel Virtual Machine - EuroPVM'96, Third European PVM Conference, München, Germany, October 7-9, 1996, Proceedings, pp. 116-125, 1996, Springer, 3-540-61779-5. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
23 | Robert Geisler, Marcus Klar, Felix Cornelius |
InterACT: An Interactive Theorem Prover for Algebraic Specifications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AMAST ![In: Algebraic Methodology and Software Technology, 5th International Conference, AMAST '96, Munich, Germany, July 1-5, 1996, Proceedings, pp. 563-566, 1996, Springer, 3-540-61463-X. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
23 | Chandrabose Aravindan |
DisLoP: A Disjunctive Logic Programming System Based on PROTEIN Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
KI ![In: KI-96: Advances in Artificial Intelligence, 20th Annual German Conference on Artificial Intelligence, Dresden, Germany, September 17-19, 1996, Proceedings, pp. 19-23, 1996, Springer, 3-540-61708-6. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
23 | Roderick Moten |
Nuprl as a concurrent interactive theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
African Americans in Mathematics ![In: African Americans in Mathematics, Proceedings of a DIMACS Workshop, Piscataway, New Jersey, USA, June 26-28, 1996, pp. 149-154, 1996, DIMACS/AMS, 978-0-8218-1142-9. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
23 | Dongming Wang 0001 |
GEOTHER: A Geometry Theorem Prover. ![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. 166-170, 1996, Springer, 3-540-61511-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
23 | Bernhard Beckert, Reiner Hähnle, Peter Oel, Martin Sulzmann |
The Tableau-based Theorem Prover 3TAP Version 4.0. ![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. 303-307, 1996, Springer, 3-540-61511-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
23 | Shie-Jue Lee, David A. Plaisted |
Controlling the Consumption of Storage with Sliding Priority Search in a Hyper-Linking Based Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. Artif. Intell. ![In: Comput. Artif. Intell. 14(6), pp. 563-578, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP BibTeX RDF |
|
23 | Jérôme Mengin |
A Theorem Prover for Default Logic Based on Prioritized Conflict Resolution and an Extended Resolution Principle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ECSQARU ![In: Symbolic and Quantitative Approaches to Reasoning and Uncertainty, European Conference, ECSQARU'95, Fribourg, Switzerland, July 3-5, 1995, Proceedings, pp. 301-310, 1995, Springer, 3-540-60112-0. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
23 | Pascal Nicolas, Béatrice Duval |
A Theorem Prover for Lukaszewicz' Open Default Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ECSQARU ![In: Symbolic and Quantitative Approaches to Reasoning and Uncertainty, European Conference, ECSQARU'95, Fribourg, Switzerland, July 3-5, 1995, Proceedings, pp. 311-319, 1995, Springer, 3-540-60112-0. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
23 | Anna Formica, Michele Missikoff, Roberto Terenzi |
A Theorem Prover for Checking Satisfiability of Object-Oriented Database Schemas. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICLP ![In: Logic Programming, Proceedings of the Twelfth International Conference on Logic Programming, Tokyo, Japan, June 13-16, 1995, pp. 819, 1995, MIT Press, 0-262-69177-9. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP BibTeX RDF |
|
23 | Laurence Pierre |
Describing and verifying synchronous circuits with the Boyer-Moore theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CHARME ![In: Correct Hardware Design and Verification Methods, IFIP WG 10.5 Advanced Research Working Conference, CHARME '95, Frankfurt/Main, Germany, October 2-4, 1995, Proceedings, pp. 35-55, 1995, Springer, 3-540-60385-9. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
23 | Slim Abdennadher, François Bry, Norbert Eisinger, Tim Geisler |
The theorem prover SATCHMO : strategies, heuristics and applications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JFPLC ![In: JFPLC'95, IVèmes Journées Francophones de Programmation en Logique & Journée d'étude Programmation par Contraintes et applications industrielles, 17-19 mai 1995, Dijon, France, pp. 349-, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP BibTeX RDF |
|
23 | Johann Schumann |
Using the Theorem Prover SETHEO for Verifying the Development of a Communication Protocol in FOCUS: A Case Study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Theorem Proving with Analytic Tableaux and Related Methods, 4th International Workshop, TABLEAUX '95, Schloß Rheinfels, St. Goar, Germany, May 7-10, 1995, Proceedings, pp. 338-352, 1995, Springer, 3-540-59338-1. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
23 | Pascal Nicolas, Béatrice Duval |
Lukaszewicz' Default Logic: A Theorem Prover Based on SLD-Resolution for Open Default Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
WOCFAI ![In: Proceedings of the Second World Conference on the Fundamentals of Artificial Intelligence, WOCFAI 1995, 3-7 July 1995, Paris, France., pp. 281-293, 1995, Angkor, 6, rue Maître-Albert, 75005 Paris, France, 2-87892-009-0. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP BibTeX RDF |
|
23 | Shie-Jue Lee, David A. Plaisted |
Problem Solving by Searching for Models with a Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Artif. Intell. ![In: Artif. Intell. 69(1-2), pp. 205-233, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
23 | Shie-Jue Lee, Chih-Hung Wu |
Improving the Efficiency of a Hyperlinking-Based Theorem Prover by Incremental Evaluation with Network Structures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 12(3), pp. 359-388, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
23 | Lawrence C. Paulson |
Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow) ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1994 |
DOI RDF |
|
23 | Alberto Artosi, Paola Cattabriga, Guido Governatori |
KED: A Deontic Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICLP Workshop: Legal Application of Logic Programming ![In: ICLP 1994 Workshop W12: Legal Application of Logic Programming, Santa Margherita Ligure, Italy, June 1994, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP BibTeX RDF |
|
23 | Joakim von Wright |
Program Refinement by Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Refine ![In: 6th Refinement Workshop, Proceedings of the 6th Refinement Workshop, organised by BCS-FACS, London, UK, 5-7 January 1994, pp. 121-150, 1994, Springer, 978-3-540-19886-4. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
23 | Alessandro Armando, Enrico Giunchiglia |
Embedding Complex Decision Procedures Inside an Interactive Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Ann. Math. Artif. Intell. ![In: Ann. Math. Artif. Intell. 8(3-4), pp. 475-502, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
23 | Lawrence C. Paulson |
The Foundation of a Generic Theorem Prover ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR cs.LO/9301105, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP BibTeX RDF |
|
23 | Lawrence C. Paulson |
Designing a Theorem Prover ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR cs.LO/9301110, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP BibTeX RDF |
|
23 | Javier Leach, Susana Nieva |
Foundations of a theorem prover for functional and mathematical uses. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Appl. Non Class. Logics ![In: J. Appl. Non Class. Logics 3(1), pp. 7-38, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
23 | J. E. Heaton, Pavel Kocura |
Presenting a Pierce Logic Based Inference Engine and Theorem Prover for Conceptual Graphs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCS ![In: Conceptual Graphs for Knowledge Representation, ICCS '93, Quebec City, Canada, August 4-7, 1993, Proceedings, pp. 381-400, 1993, Springer, 3-540-56979-0. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
23 | Shie-Jue Lee, Chih-Hung Wu |
Improving Efficiency of a Theorem Prover by Eliminating Redundant Unifications Using Network Structures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCI ![In: Computing and Information - ICCI'93, Fifth International Conference on Computing and Information, Sudbury, Ontario, Canada, May 27-29, 1993, Proceedings, pp. 299-304, 1993, IEEE Computer Society, 0-8186-4212-2. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP BibTeX RDF |
|
23 | John K. Slaney |
SCOTT: A Model-Guided Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAI ![In: Proceedings of the 13th International Joint Conference on Artificial Intelligence. Chambéry, France, August 28 - September 3, 1993, pp. 109-115, 1993, Morgan Kaufmann, 1-55860-300-X. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP BibTeX RDF |
|
23 | Richard J. Boulton |
Efficiency in a fully-expansive theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1993 |
RDF |
|
23 | Reiner Hähnle, Bernhard Beckert, Stefan Gerberding, Werner Kernig |
The Many-Valued Theorem Prover 3TAP. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IWBS Report ![In: IWBS Report 227, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
RDF |
|
23 | Mark E. Stickel |
A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 104(1), pp. 109-128, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | James D. Baker, Shariar Zand-Biglari |
An Integral Theorem Prover And The Role Of Proof Planning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 8(2), pp. 275-295, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Reinhold Letz, Johann Schumann, Stefan Bayerl, Wolfgang Bibel |
SETHEO: A High-Performance Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 8(2), pp. 183-212, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Soumitra Bose, Edmund M. Clarke, David E. Long, Spiro Michaylov |
PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 8(2), pp. 153-181, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Matt Kaufmann |
An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 9(3), pp. 355-372, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Dan Sahlin, Torkel Franzén, Seif Haridi |
An Intuitionistic Predicate Logic Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Log. Comput. ![In: J. Log. Comput. 2(5), pp. 619-656, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Ursula Martin, Michael Lai |
Some Experiments with a Completion Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Symb. Comput. ![In: J. Symb. Comput. 13(1), pp. 81-100, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Javier Leach, Susana Nieva |
MIZ-PR: A Theorem Prover for Polymorphic and Recursive Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, pp. 481-483, 1992, Springer, 3-540-55727-X. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Adel Bouhoula, Emmanuel Kounalis, Michaël Rusinowitch |
SPIKE, an Automatic Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, pp. 460-462, 1992, Springer, 3-540-55727-X. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Monica Nesi |
Formalizing a Modal Logic for CSS in the HOL Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992, pp. 279-294, 1992, North-Holland/Elsevier, 0-444-89880-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
23 | Manfred R. Jobmann, Johann Schumann |
Modelling and Performances Analysis of a Parallel Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SIGMETRICS ![In: Proceedings of the 1992 ACM SIGMETRICS joint international conference on Measurement and modeling of computer systems, Newport, Rhode Island, USA, June 1-5, 1992, pp. 259-260, 1992, ACM, 0-89791-507-0. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Dave Barker-Plummer, Alex Rothenberg |
The GAZER Theorem Prover. ![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. 726-730, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Bernhard Beckert, Stefan Gerberding, Reiner Hähnle, Werner Kernig |
The Tableau-Based Theorem Prover 3TAP for Multi-Valued Logics. ![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. 758-760, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Ewing L. Lusk, William McCune, John K. Slaney |
ROO: A Parallel Theorem Prover. ![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. 731-734, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | 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 |
|
23 | Edmund M. Clarke, Xudong Zhao 0005 |
Analytica - A Theorem Prover in Mathematica. ![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. 761-765, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Johann Schumann |
KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract). ![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. 740-742, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
23 | Mark Bickford, Mandayam K. Srivas |
Verification of a Fault-Tolerant Property of a Multiprocessor System: A Case Study in Theorem Prover-Based Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPCD ![In: Theorem Provers in Circuit Design, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, The Netherlands, 22-24 June 1992, Proceedings, pp. 225-251, 1992, North-Holland, 0-444-89686-4. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
23 | Holger Busch |
Transformational Design in a Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPCD ![In: Theorem Provers in Circuit Design, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, The Netherlands, 22-24 June 1992, Proceedings, pp. 175-196, 1992, North-Holland, 0-444-89686-4. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
23 | Philippe Lamarre |
A Tableau Like Theorem Prover for Conditional Logics (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. 52-55, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
23 | Wilfried Neitz |
A Connection Method based Theorem Prover with Selective Backtracking (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. 59-60, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
23 | Charles G. Morgan |
An Automated Theorem Prover for Relational Logic (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. 56-58, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
23 | Philippe Lamarre |
A Promenade from Monotonicity to Non-Monotonicity Following a Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
KR ![In: Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR'92). Cambridge, MA, USA, October 25-29, 1992., pp. 572-580, 1992, Morgan Kaufmann, 1-55860-262-3. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
23 | Manfred R. Jobmann, Johann Schumann |
Modelling and performance analysis of a parallel theorem prover ![Search on Bibsonomy](Pics/bibsonomy.png) |
Forschungsberichte, TU Munich ![In: Forschungsberichte, TU Munich TUM I 9129, pp. 1-17, 1991. The full citation details ...](Pics/full.jpeg) |
1991 |
RDF |
|
23 | Wen-Tsuen Chen, Tzren-Ru Chou, Kuen-Rong Hsieh, Huai-Jen Liu |
Design of a Parallel Theorem Prover for First Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Inf. Sci. Eng. ![In: J. Inf. Sci. Eng. 7(3), pp. 385-403, 1991. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP BibTeX RDF |
|
23 | Christine Lafontaine, Yves Ledru, Pierre-Yves Schobbens |
An Experiment in Formal Software Development: Using the B Theorem Prover on a VDM Case Study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Commun. ACM ![In: Commun. ACM 34(5), pp. 62-71, 1991. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
23 | Laurent Catach |
TABLEAUX: A General Theorem Prover for Modal Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 7(4), pp. 489-510, 1991. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
23 | Manfred R. Jobmann, Johann Schumann |
Modelling and performance Analysis of a Parallel Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MMB ![In: Messung, Modellierung und Bewertung von Rechensystemen, 6. GI/ITG-Fachtagung, 18.-20. September 1991, Neubiberg, Deutschland, Proceedings, pp. 228-243, 1991, Springer, 3-540-54550-6. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
23 | Hiroshi Fujita 0002, Ryuzo Hasegawa |
A Model Generation Theorem Prover in KL1 Using a Ramified -Stack Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICLP ![In: Logic Programming, Proceedings of the Eigth International Conference, Paris, France, June 24-28, 1991, pp. 535-548, 1991, MIT Press, 0-262-56058-5. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP BibTeX RDF |
|
23 | Wen-Tsuen Chen, Tzren-Ru Chou, Kuen-Rong Hsieh, Huai-Jen Liu |
Design of a parallel theorem prover for first order logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
COMPSAC ![In: Proceedings of the Fifteenth Annual International Computer Software and Applications Conference, COMPSAC 1991, Tokyo, Japan, 11-13 September, 1991, pp. 275-280, 1991, IEEE, 0-8186-2152-4. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
23 | Christian B. Suttner, Wolfgang Ertel |
Using connectionist networks for guiding the search of a theorem prover ![Search on Bibsonomy](Pics/bibsonomy.png) |
Forschungsberichte, TU Munich ![In: Forschungsberichte, TU Munich TUM I 9011, pp. 1-18, 1990. The full citation details ...](Pics/full.jpeg) |
1990 |
RDF |
|
23 | Johann Schumann, Reinhold Letz |
PARTHEO: a high performance parallel theorem prover ![Search on Bibsonomy](Pics/bibsonomy.png) |
Forschungsberichte, TU Munich ![In: Forschungsberichte, TU Munich TUM I 9009, pp. 1-17, 1990. The full citation details ...](Pics/full.jpeg) |
1990 |
RDF |
|
23 | Albert John Camilleri |
Reasoning in CSP via the HOL theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Jerusalem Conference on Information Technology ![In: Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, Jerusalem, October 22-25, 1990, pp. 173-183, 1990, IEEE Computer Society, 0-8186-2078-1. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
23 | Christian B. Suttner |
A Parallel Theorem Prover with Heuristic Work Distribution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Dagstuhl Seminar on Parallelization in Inference Systems ![In: Parallelization in Inference Systems, International Workshop, Dagstuhl Castle, Germany, December 17-18, 1990, Proceedings, pp. 243-252, 1990, Springer, 3-540-55425-4. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
23 | Christian B. Suttner |
Representing Heuristic-Relevant Information for an Automated Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IMYCS ![In: Aspects and Prospects of Theoretical Computer Science, 6th International Meeting of Young Computer Scientists, Smolenice, Czechoslovakia, November 19-23, 1990, Proceedings, pp. 261-270, 1990, Springer, 3-540-53414-8. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
23 | Neil V. Murray, Erik Rosenthal |
DISSOLVER: A Dissolution-based Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 665-666, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
23 | Ralph Butler, Ian T. Foster, Anita Jindal, Ross A. Overbeek |
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. 649-650, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
23 | Mark E. Stickel |
A 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. 673-674, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
23 | Geoff Sutcliffe |
A General Clause Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 675-676, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|