|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 1960 occurrences of 846 keywords
|
|
|
Results
Found 3383 publication records. Showing 3383 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
40 | Raymond Reiter |
A Semantically Guided Deductive System for Automatic Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 25(4), pp. 328-334, 1976. The full citation details ...](Pics/full.jpeg) |
1976 |
DBLP DOI BibTeX RDF |
semantics, theorem proving, Natural deduction |
39 | D. Andre de Waal, John P. Gallagher |
The Applicability of Logic Program Analysis and Transformation to Theorem Proving. ![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. 207-221, 1994, Springer, 3-540-58156-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
39 | Matthias Baaz, Agata Ciabattoni, Christian G. Fermüller |
Herbrand's Theorem for Prenex Gödel Logic and its Consequences for Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings, pp. 201-215, 2001, Springer, 3-540-42957-3. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
39 | J Strother Moore |
Inductive assertions and operational semantics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 8(4-5), pp. 359-371, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Theorem proving, JVM, Software verification, Verification condition |
39 | Leo Freitas, Jim Woodcock 0001, Ana Cavalcanti 0001 |
State-rich model checking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Innov. Syst. Softw. Eng. ![In: Innov. Syst. Softw. Eng. 2(1), pp. 49-64, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Formal method tools, Model checking, Theorem proving, Abstract interpretation |
39 | Richard Sommer, Gregory Nuckols |
A Proof Environment for Teaching Mathematics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 32(3), pp. 227-258, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
EPGY Theorem Proving Environment, computer-based learning, automated reasoning |
39 | Noboru Matsuda, Kurt VanLehn |
GRAMY: A Geometry Theorem Prover Capable of Construction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 32(1), pp. 3-33, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
automated geometry theorem proving, search control, intelligent tutoring system, constraint satisfaction problem, construction |
39 | Silvio do Lago Pereira, Leliane Nunes de Barros |
Planning with Abduction: A Logical Framework to Explore Extensions to Classical Planning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBIA ![In: Advances in Artificial Intelligence - SBIA 2004, 17th Brazilian Symposium on Artificial Intelligence, São Luis, Maranhão, Brazil, September 29 - October 1, 2004, Proceedings, pp. 62-72, 2004, Springer, 3-540-23237-0. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
planning, theorem proving, abduction, event calculus |
39 | Michael J. C. Gordon |
Validating the PSL/Sugar Semantics Using Automated Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 15(4), pp. 406-421, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Accellera, Property language, Sugar, Model checking, Semantics, Formal verification, Theorem proving, Higher-order logic, PSL, HOL |
39 | Eric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen 0002 |
Proof Search and Proof Check for Equational and Inductive Theorems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, pp. 297-316, 2003, Springer, 3-540-40559-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
proof terms, computation, induction, automated theorem proving, deduction, rewrite rules, proof assistant |
39 | Francis Alexandre, Khaled Bsaïes, Moussa Demba |
Predicate Synthesis from Inductive Proof Attempt of Faulty Conjectures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LOPSTR ![In: Logic Based Program Synthesis and Transformation, 13th International Symposium LOPSTR 2003, Uppsala, Sweden, August 25-27, 2003, Revised Selected Papers, pp. 20-33, 2003, Springer, 3-540-22174-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Corrective predicate, implicative formulas, folding/unfolding rules, theorem proving, program synthesis, abduction |
39 | Adel Bouhoula |
Sufficient Completeness and Parameterized Proofs by Induction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ALP ![In: Algebraic and Logic Programming, 4th International Conference, ALP'94, Madid, Spain, September 14-16, 1994, Proceedings, pp. 23-40, 1994, Springer, 3-540-58431-5. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
Implicit induction, Parameterized Conditional Specifications, Theorem Proving, Term rewriting systems, Sufficient completeness |
39 | Jean Goubault |
The Complexity of Resource-Bounded First-Order Classical Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STACS ![In: STACS 94, 11th Annual Symposium on Theoretical Aspects of Computer Science, Caen, France, February 24-26, 1994, Proceedings, pp. 59-70, 1994, Springer, 3-540-57785-8. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
Topics computational complexity, computational issues in AI (automated theorem proving), logics |
39 | Richard C. Potter, David A. Plaisted |
Term Rewriting: Some Experimental Results. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 435-453, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
Theorem proving, set theory, term rewriting |
39 | Douglas J. Howe |
Computational Metatheory in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 238-257, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
formal metamathematics, reflection, Theorem proving, type theory, constructive mathematics, tactics |
38 | Josef Urban |
MPTP - Motivation, Implementation, First Experiments. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 33(3-4), pp. 319-339, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
ATP, Mizar, MPA, MPTP |
38 | Julien Schmaltz, Dominique Borrione |
A functional formalization of on chip communications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 20(3), pp. 241-258, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Formal methods, Networks on chip, Automated theorem proving, Communication architectures |
38 | Peter Baumgartner 0001, Ulrich Furbach, Margret Groß-Hardt, Alex Sinner |
Living Book - Deduction, Slicing, and Interaction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 32(3), pp. 259-286, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
knowledge management, e-learning, knowledge representation, theorem proving |
38 | Achim D. Brucker, Burkhart Wolff |
Using Theory Morphisms for Implementing Formal Methods Tools. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers, pp. 59-77, 2002, Springer, 3-540-14031-X. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Shallow Embeddings, Formal Methods, Theorem Proving, OCL, Formal Semantics |
37 | Yiming Xu, Michael Norrish |
Dependently Sorted Theorem Proving for Mathematical Foundations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 33:1-33:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
37 | Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann |
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 12:1-12:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
37 | Mario Carneiro, Chad E. Brown, Josef Urban |
Automated Theorem Proving for Metamath. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, pp. 9:1-9:19, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-284-6. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
37 | Jeremy Avigad, Assia Mahboubi |
Erratum to: Interactive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
37 | Nathan Fulton, Stefan Mitsch, Rose Bohrer, André Platzer |
Bellerophon: Tactical Theorem Proving for Hybrid Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 207-224, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
37 | Moa Johansson |
Automated Theory Exploration for Interactive Theorem Proving: - An Introduction to the Hipster System. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, pp. 1-11, 2017, Springer, 978-3-319-66106-3. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
37 | Joachim Breitner |
Visual Theorem Proving with the Incredible Proof Machine. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings, pp. 123-139, 2016, Springer, 978-3-319-43143-7. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
37 | Roderick Chapman, Florian Schanda |
Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, pp. 17-26, 2014, Springer, 978-3-319-08969-0. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
37 | Martin Ring, Christoph Lüth |
Collaborative Interactive Theorem Proving with Clide. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, pp. 467-482, 2014, Springer, 978-3-319-08969-0. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
37 | Panagiotis Manolios |
Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 18, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
37 | Makarius Wenzel |
Shared-Memory Multiprocessing for Interactive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 418-434, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
37 | K. Rustan M. Leino |
Automating Theorem Proving with SMT. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 2-16, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
37 | Phil Scott, Jacques D. Fleuriot |
Composable Discovery Engines for Interactive Theorem Proving. ![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. 370-375, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
37 | Mike Gordon |
Twenty Years of Theorem Proving for HOLs Past, Present and Future. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 1-5, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
37 | Lawrence C. Paulson, Kong Woei Susanto |
Source-Level Proof Reconstruction for Interactive Theorem Proving. ![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. 232-245, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
37 | Behzad Akbarpour, Sofiène Tahar |
Error Analysis of Digital Filters Using Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings, pp. 1-17, 2004, Springer, 3-540-23017-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
37 | Silvio Ranise, David Déharbe |
Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs. ![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. 105-119, 2003, Elsevier. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
37 | David Delahaye |
Free-Style Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 164-181, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
37 | Micaela Mayero |
Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm). ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 246-262, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
37 | Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, Sam Owre |
Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 27-42, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
37 | Jason Hickey, Aleksey Nogin |
Fast Tactic-Based Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 252-267, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
37 | Don Syme |
Three Tactic Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, pp. 203-220, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
37 | Thomas Kropf |
Recent Advancements in Hardware Verification - How to Make Theorem Proving Fit for an Industrial Usage. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, pp. 1-4, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
37 | Friedrich W. von Henke, Stephan Pfab, Holger Pfeifer, Harald Rueß |
Case Studies in Meta-Level Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, pp. 461-478, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
37 | Myla Archer, Constance L. Heitmeyer |
Human-Style Theorem Proving Using PVS. ![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. 33-48, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
37 | Jeremy V. Pitt, Jim Cunningham |
Distributed Modal Theorem Proving with KE. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Theorem Proving with Analytic Tableaux and Related Methods, 5th International Workshop, TABLEAUX '96, Terrasini, Palermo, Italy, May 15-17, 1996, Proceedings, pp. 160-176, 1996, Springer, 3-540-61208-4. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
37 | Wolfgang Bibel, Stefan Brüning, Uwe Egly, Daniel S. Korn, Thomas Rath |
Issues in Theorem Proving Based on the Connection Method. ![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. 1-16, 1995, Springer, 3-540-59338-1. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
37 | Holger Busch |
First-Order Automation for Higher-Order-Logic Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings, pp. 97-112, 1994, Springer, 3-540-58450-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
37 | Richard J. Boulton |
A Lazy Approach to Fully-Expansive Theorem Proving. ![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. 19-38, 1992, North-Holland/Elsevier, 0-444-89880-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
37 | Jim Cunningham, Marcello D'Agostino, Jeremy V. Pitt |
Towards Tableau Theorem-Proving with Analytic Cut. ![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. 23-25, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
37 | Vincent Risch, Camilla Schwind |
Tableaux-Based Theorem Proving and Non-Standard Reasoning. ![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. 76-78, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
37 | Zoran Ognjanovic, Dragan Urosevic, Tatjana Petrovic, Zorana Ristovic |
A Tableaux Retlated Method for Modal Theorem Proving (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. 61-63, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
37 | Oliver Bittel |
The Lambda-Tableau Calculus: A New Approach to Theorem Proving in the Intuitionistic Logic (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. 15-18, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
37 | Simon Bainbridge, Albert John Camilleri, Roger Fleming |
Industrial Application of Theorem Proving to System Level Design. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA, pp. 130-142, 1991, IEEE Computer Society. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP BibTeX RDF |
|
37 | Marta Franová |
Constructive Matching - A Methodology for Inductive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in AI, European Workshop, JELIA '90, Amsterdam, The Netherlands, September 10-14, 1990, Proceedings, pp. 212-226, 1990, Springer, 3-540-53686-8. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
36 | Viorica Sofronie-Stokkermans |
Automated theorem proving by resolution in non-classical logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Ann. Math. Artif. Intell. ![In: Ann. Math. Artif. Intell. 49(1-4), pp. 221-252, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Mathematics Subject Classifications (2000) 06D(05, 25,30,35,50), 03G(10,20) |
36 | Arjen Hommersom, Peter J. F. Lucas, Michael Balser |
Meta-level Verification of the Quality of Medical Guidelines Using Interactive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27-30, 2004, Proceedings, pp. 654-666, 2004, Springer, 3-540-23242-7. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
36 | Alexander V. Lyaletski, Andrey Paskevich, Konstantin Verchinine |
Theorem Proving and Proof Verification in the System SAD. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings, pp. 236-250, 2004, Springer, 3-540-23029-7. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
36 | Vijay Chandru, Jean-Louis Lassez |
Qualitative Theorem Proving in Linear Constraints. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Verification: Theory and Practice ![In: Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, pp. 395-406, 2003, Springer, 3-540-21002-4. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
36 | 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 |
|
36 | Gérard P. Huet |
Higher Order Unification 30 Years Later. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 3-12, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
36 | Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov |
On the Evaluation of Indexing Techniques for Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, pp. 257-271, 2001, Springer, 3-540-42254-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
36 | Steven D. Johnson |
View from the Fringe of the Fringe (Joint with CHARME 2001). ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 4, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
36 | Ricardo Caferra, Nicolas Peltier, François Puitg |
Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry, Third International Workshop, ADG 2000, Zurich, Switzerland, September 25-27, 2000, Revised Papers, pp. 268-305, 2000, Springer, 3-540-42598-5. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Automated geometric reasoning, model (counter-example) building, proof structuring with diagrams, analogy, computer assisted learning |
36 | Peter B. Andrews, Matthew Bishop, Chad E. Brown |
System Description: TPS: A Theorem Proving System for Type Theory. ![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. 164-169, 2000, Springer, 3-540-67664-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
36 | Natarajan Shankar |
Combining Theorem Proving and Model Checking through Symbolic Analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CONCUR ![In: CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, pp. 1-16, 2000, Springer, 3-540-67897-2. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
36 | Maria Paola Bonacina |
A Taxonomy of Theorem-Proving Strategies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Artificial Intelligence Today ![In: Artificial Intelligence Today: Recent Trends and Developments, pp. 43-84, 1999, Springer, 3-540-66428-9. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
36 | Haiyan Xiong, Paul Curzon, Sofiène Tahar |
Importing MDG Verification Results into HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, pp. 293-310, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
36 | Erica Melis, Jon Whittle 0001 |
Internal Analogy in Theorem Proving. ![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. 92-105, 1996, Springer, 3-540-61511-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
36 | Wai Wong |
Recording and Checking HOL Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995, Proceedings, pp. 353-368, 1995, Springer, 3-540-60275-5. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
36 | Maritta Heisel, Wolfgang Reif, Werner Stephan 0001 |
Tactical Theorem Proving in Program Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 117-131, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
36 | Wen-Tsuen Chen, Ming-Yi Fang |
Theorem proving in propositional logic on vector computers using a generalized Davis-Putnam procedure. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SC ![In: Proceedings Supercomputing '90, New York, NY, USA, November 12-16, 1990, pp. 658-665, 1990, IEEE Computer Society, 0-89791-412-0. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
36 | Cliff B. Jones, Richard C. Moore |
MUFFIN: A User Interface Design Experiment for a Theorem Proving Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VDM Europe ![In: VDM '88, VDM - The Way Ahead, 2nd VDM-Europe Symposium, Dublin, Ireland, September 11-16, 1988, Proceedings, pp. 337-375, 1988, Springer, 3-540-50214-9. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
|
36 | Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek |
Paths to High-Performance Automated Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings, pp. 588-597, 1986, Springer, 3-540-16780-3. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP DOI BibTeX RDF |
|
36 | Jieh Hsiang |
Two Results in Term Rewriting Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, First International Conference, RTA-85, Dijon, France, May 20-22, 1985, Proceedings, pp. 301-324, 1985, Springer, 3-540-15976-2. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
|
35 | Tomás Recio, Francisco Botana |
Where the Truth Lies (in Automatic Theorem Proving in Elementary Geometry). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCSA (2) ![In: Computational Science and Its Applications - ICCSA 2004, International Conference, Assisi, Italy, May 14-17, 2004, Proceedings, Part II, pp. 761-770, 2004, Springer, 3-540-22056-9. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
35 | Nancy A. Day, Jeffrey J. Joyce |
Symbolic Functional Evaluation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, pp. 341-358, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
35 | 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 |
35 | Mark E. Stickel |
A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings, pp. 248-258, 1984, Springer, 3-540-96022-8. The full citation details ...](Pics/full.jpeg) |
1984 |
DBLP DOI BibTeX RDF |
|
35 | James R. Slagle |
Automatic Theorem Proving With Renamable and Semantic Resolution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 14(4), pp. 687-697, 1967. The full citation details ...](Pics/full.jpeg) |
1967 |
DBLP DOI BibTeX RDF |
|
35 | Richard J. Waldinger |
Whatever Happened to Deductive Question Answering? ![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. 15-16, 2007, Springer, 978-3-540-75558-6. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
35 | Volker Sorge, Andreas Meier 0002, Roy L. McCasland, Simon Colton |
Automatic Construction and Verification of Isotopy Invariants. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 40(2-3), pp. 221-243, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Automated mathematics, Classification theorems, Computer algebra, Automated theorem proving, Model generation, SAT solving, Invariant generation, Isotopy |
35 | 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 |
34 | David C. J. Matthews, Makarius Wenzel |
Efficient parallel programming in Poly/ML and Isabelle/ML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DAMP ![In: Proceedings of the POPL 2010 Workshop on Declarative Aspects of Multicore Programming, DAMP 2010, Madrid, Spain, January 19, 2010, pp. 53-62, 2010, ACM, 978-1-60558-859-9. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
parallel standard ml, poly/ml, theorem proving applications, data parallelism, isabelle |
34 | Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif |
Bounded Relational Analysis of Free Data Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TAP ![In: Tests and Proofs - 2nd International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings, pp. 99-115, 2008, Springer, 978-3-540-79123-2. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
SAT checking, model checking, verification, formal methods, theorem proving, First-order logic, abstract data types |
34 | Yves Bertot, Vladimir Komendantsky |
Fixed point semantics and partial recursion in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 15-17, 2008, Valencia, Spain, pp. 89-96, 2008, ACM, 978-1-60558-117-0. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
least fixed point semantics, non-terminating functions, program extraction, the Knaster-Tarski theorem, automated theorem proving |
34 | Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon |
Proof producing synthesis of arithmetic and cryptographic hardware. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 19(3), pp. 343-362, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Cryptography, Compiling, Theorem proving, Hardware synthesis, High assurance |
34 | Osman Hasan, Sofiène Tahar |
Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFM ![In: Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings, pp. 333-352, 2007, Springer, 978-3-540-73209-9. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Higher-Order-Logic, Interactive Theorem Proving, HOL, Probabilistic Systems, Cumulative Distribution Function |
34 | Jim Woodcock 0001, Leo Freitas |
Z/Eves and the Mondex Electronic Purse. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAC ![In: Theoretical Aspects of Computing - ICTAC 2006, Third International Colloquium, Tunis, Tunisia, November 20-24, 2006, Proceedings, pp. 15-34, 2006, Springer, 3-540-48815-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
electronic finance, software archaeology, the Z notation, Z/Eves, security, refinement, theorem proving, smart cards, Grand Challenge, Verified Software Repository, Mondex |
34 | Achim D. Brucker, Burkhart Wolff |
Interactive Testing with HOL-TestGen. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FATES ![In: Formal Approaches to Software Testing, 5th International Workshop, FATES 2005, Edinburgh, UK, July 11, 2005, Revised Selected Papers, pp. 87-102, 2005, Springer, 3-540-34454-3. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
symbolic test case generations, theorem proving, black box testing, white box testing, interactive testing |
34 | Tjark Weber |
Towards Mechanized Program Verification with Separation Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, pp. 250-264, 2004, Springer, 3-540-23024-6. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
Separation Logic, Interactive Theorem Proving, Formal Program Verification |
34 | Sandeep S. Kulkarni, Borzoo Bonakdarpour, Ali Ebnenasir |
Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LOPSTR ![In: Logic Based Program Synthesis and Transformation, 14th International Symposium, LOPSTR 2004, Verona, Italy, August 26-28, 2004, Revised Selected Papers, pp. 36-52, 2004, Springer, 3-540-26655-0. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
Addition of faulttolerance, Fault-tolerance, Program transformation, Theorem proving, Program synthesis, PVS, Mechanical verification |
34 | Lars-Åke Fredlund, Dilian Gurov, Thomas Noll 0001, Mads Dam, Thomas Arts, Gennady Chugunov |
A verification tool for ERLANG. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 4(4), pp. 405-420, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Formal methods, Theorem proving, Software verification |
34 | Stefan Blom, Jaco van de Pol |
State Space Reduction by Proving Confluence. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, pp. 596-609, 2002, Springer, 3-540-43997-8. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
on-the-fly state space reduction, symbolic transformation, 7CRL tool set, theorem proving, Labeled transition systems, partial order reduction, confluence, branching bisimulation |
34 | Michael W. Whalen, Johann Schumann, Bernd Fischer 0002 |
Synthesizing Certified Code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings, pp. 431-450, 2002, Springer, 3-540-43928-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
automatic program synthesis, code certification, program verification, automated theorem proving, proof-carrying code |
34 | Jeremy E. Dawson, Rajeev Goré |
Machine-Checking the Timed Interval Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Australian Joint Conference on Artificial Intelligence ![In: AI 2002: Advances in Artificial Intelligence, 15th Australian Joint Conference on Artificial Intelligence, Canberra, Australia, December 2-6, 2002, Proceedings, pp. 95-106, 2002, Springer, 3-540-00197-2. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Reasoning about time, theorem proving, automated reasoning |
34 | Christoph Kern, Tarik Ono-Tesfaye, Mark R. Greenstreet |
A light-weight framework for hardware verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 3(3), pp. 286-313, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
Refinement, Theorem-proving, Timing verification, Switch-level models, SRT division |
34 | Andrea Formisano 0001, Eugenio G. Omodeo, Marco Temperini |
Instructing Equational Set-Reasoning with Otter. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, pp. 152-167, 2001, Springer, 3-540-42254-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
Set reasoning, map algebra, first-order theorem proving |
34 | Alexandre Riazanov, Andrei Voronkov |
Partially Adaptive Code Trees. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in Artificial Intelligence, European Workshop, JELIA 2000 Malaga, Spain, September 29 - October 2, 2000, Proceedings, pp. 209-223, 2000, Springer, 3-540-41131-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
term indexing, code trees, matching, automated theorem proving, subsumption |
34 | Andrea Formisano 0001, Eugenio G. Omodeo |
An Equational Re-engineering of Set Theories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FTP (LNCS Selection) ![In: Automated Deduction in Classical and Non-Classical Logics, Selected Papers, pp. 175-190, 1998, Springer, 3-540-67190-0. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
first-order theorem-proving, relation algebras, Set Theory, algebraic logic |
34 | David von Oheimb, Thomas F. Gritzner |
RALL: Machine-Supported Proofs for Relation Algebra. ![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. 380-394, 1997, Springer, 3-540-63104-6. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
interactive and automatic theorem proving, atom structure, Relation algebra, Isabelle |
Displaying result #101 - #200 of 3383 (100 per page; Change: ) Pages: [ <<][ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ 11][ >>] |
|