Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
97 | Piergiorgio Bertoli, Jacques Calmet, Fausto Giunchiglia, Karsten Homann |
Specification and Integration of Theorem Provers and Computer Algebra Systems. |
AISC |
1998 |
DBLP DOI BibTeX RDF |
Integration, Theorem Provers, Computer Algebra Systems, Formal Frameworks |
75 | Alexander Leitsch |
Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction. |
FTP (LNCS Selection) |
1998 |
DBLP DOI BibTeX RDF |
|
67 | Amy P. Felty, Dale Miller 0001 |
Specifying Theorem Provers in a Higher-Order Logic Programming Language. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
66 | Clemens Ballarin, Lawrence C. Paulson |
Reasoning About Coding Theory: The Benefits We Get from Computer Algebra. |
AISC |
1998 |
DBLP DOI BibTeX RDF |
mechanised reasoning, combining systems, soundness of computer algebra systems, specialisation problem, AISC topics, Integration of logical reasoning and computer algebra, Computer algebra, coding theory, automated theorem provers |
61 | Josef Urban |
MPTP - Motivation, Implementation, First Experiments. |
J. Autom. Reason. |
2004 |
DBLP DOI BibTeX RDF |
ATP, Mizar, MPA, MPTP |
61 | Predrag Janicic, Alan Bundy, Ian Green |
A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
58 | Ian Horrocks 0001, Andrei Voronkov |
Reasoning Support for Expressive Ontology Languages Using a Theorem Prover. |
FoIKS |
2006 |
DBLP DOI BibTeX RDF |
|
57 | Pablo Cordero, Gloria Gutiérrez, Javier Martínez 0001, Inmaculada Perez de Guzmán |
A New Algebraic Tool for Automatic Theorem Provers. |
Ann. Math. Artif. Intell. |
2004 |
DBLP DOI BibTeX RDF |
multisemilattice, theorem provers, automated deduction, implicants, ideals, lattice theory |
57 | Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, Martin C. Rinard |
Using First-Order Theorem Provers in the Jahob Data Structure Verification System. |
VMCAI |
2007 |
DBLP DOI BibTeX RDF |
|
57 | Owen L. Astrachan, Mark E. Stickel |
Caching and Lemmaizing in Model Elimination Theorem Provers. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
54 | Krystof Hoder, Andrei Voronkov |
Comparing Unification Algorithms in First-Order Theorem Proving. |
KI |
2009 |
DBLP DOI BibTeX RDF |
|
53 | J. Santiago Jorge, Víctor M. Gulías, Laura M. Castro |
Verification of Program Properties Using Different Theorem Provers: A Case Study. |
EUROCAST |
2007 |
DBLP DOI BibTeX RDF |
|
53 | Bernhard Beckert, Sarah Grebing, Florian Böhl |
How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers. |
UITP |
2014 |
DBLP DOI BibTeX RDF |
|
53 | Victoria Stavridou, Thomas F. Melham, Raymond T. Boute (eds.) |
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 |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Keith Hanna, Neil Daeche, Gareth Howells 0001 |
Implementation of the Veritas Design Logic. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Mark Bickford, Mandayam K. Srivas |
Verification of a Fault-Tolerant Property of a Multiprocessor System: A Case Study in Theorem Prover-Based Verification. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Holger Busch |
Transformational Design in a Theorem Prover. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Simon Bainbridge, Albert John Camilleri, Roger Fleming |
Theorem Proving as an Industrial Tool for System Level Desgin. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | John Herbert |
Incremental Design and Formal Verification of Microcoded Microporcessors. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Jørgen Staunstrup, Stephen J. Garland, John V. Guttag |
Mechanized Verification of Circuit Descriptions Using the Larch Prover. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Victoria Stavridou, Joseph A. Goguen, Andrew Stevens, Steven M. Eker, Serge N. Aloneftis, Keith Michael Hobley |
FUNNEL and 2OBJ: Towards an Integrated Hardware Design Environment. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Beth Levy, Ivan Filippenko, Leo Marcus, Telis Menas |
Using the State Delta Verification System (SDVS) for Hardware Verification. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Diederik Verkest, J. Vandenbergh, Luc J. M. Claesen, Hugo De Man |
A Description Methodology for Parameterized Modules in the Boyer-Moore Logic. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Keith Hanna, Neil Daeche |
The Veritas Design Logic: A User's View. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Paul B. Jackson |
Nuprl and Its Use in Circuit Design. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Tiziana Margaria |
Hierarchical Mixed-Mode Verification of Complex FSMs Described at the RT Level. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Richard J. Boulton, Andrew D. Gordon 0001, Michael J. C. Gordon, John Harrison 0001, John Herbert, John Van Tassel |
Experience with Embedding Hardware Description Languages in HOL. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Bishop Brock, Warren A. Hunt Jr., William D. Young |
Introduction to a Formally Defined Hardware Description Language. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | Hans Henrik Løvengreen, Jørgen Staunstrup |
Synchronous Realization of Asynchronous Computations. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
53 | D. J. Kinniment, Albert Koelmans |
Modelling and Verification of Timing Conditions with the Boyer Moore Prover. |
TPCD |
1992 |
DBLP BibTeX RDF |
|
51 | David Hemer |
A systematic approach to connecting standalone theorem provers to formal development environments. |
APSEC |
2006 |
DBLP DOI BibTeX RDF |
|
49 | Peter Balsiger, Alain Heuerding |
Comparison of Theorem Provers for Modal Logics - Introduction and Summary. |
TABLEAUX |
1998 |
DBLP DOI BibTeX RDF |
|
47 | Thomas Raths, Jens Otten, Christoph Kreitz |
The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic. |
TABLEAUX |
2005 |
DBLP DOI BibTeX RDF |
|
47 | Raul H. C. Lopes, Mark Tarver |
Inducing Theorem Provers from Proofs. |
ICTAI |
1997 |
DBLP DOI BibTeX RDF |
theorem prover induction, automatic theorem prover generation, proof examples, intuitionistic propositional calculus, depth-first search strategy, loop detection, inductive generalization, machine learning, theorem proving |
45 | Sriipriya G |
Implementation methodology for using concurrent and collaborative approaches for theorem provers, with case studies of SAT and LCF style provers. |
|
2013 |
RDF |
|
44 | Perry R. James, Patrice Chalin |
Extended static checking in JML4: benefits of multiple-prover support. |
SAC |
2009 |
DBLP DOI BibTeX RDF |
ESC, ESC4, JML4, theorem provers, Java modeling language, static verification, extended static checking |
44 | Willem C. Mallon, Jan Tijmen Udding |
Using Metrics for Proof Rules for Recursively Defined Delay-insensitive Specifications. |
ASYNC |
1997 |
DBLP DOI BibTeX RDF |
delay-insensitive specifications, recursive definition, linear proofs, intuitive induction rule, algebraic specification, algebraic specifications, theorem provers, correctness proofs, proof rules, proof rule |
44 | Keith Vanderveen, C. V. Ramamoorthy |
Anytime Reasoning in First-Order Logic. |
ICTAI |
1997 |
DBLP DOI BibTeX RDF |
anytime reasoning, best-effort answers, bounded reasoning resources, S/sub 1/ approximation, S/sub 3/ approximation, most likely solution, first-order logic, formal logic, theorem provers, algorithm performance |
44 | Shiu-Kai Chin, John Faust, Joseph Giordano |
Integrating formal methods tools to support system design. |
ICECCS |
1995 |
DBLP DOI BibTeX RDF |
formal methods tools integration, top-level process descriptions, gate-level hardware designs, simulators, formal specification, system design, specification languages, specification languages, systems analysis, system engineering, theorem-provers, computer-aided design tools, model checkers |
44 | Pavel Vanousek |
Automated Theorem Proving in a Combination of Theories with Disjoint Signatures. |
SOFSEM |
1998 |
DBLP DOI BibTeX RDF |
|
44 | Mark E. Stickel |
Building Theorem Provers. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
44 | Ricardo Caferra, Michel Herment |
GLEFATINF: A Graphic Framework for Combining Theorem Provers and Editing Proofs for Different Logics. |
DISCO |
1993 |
DBLP DOI BibTeX RDF |
Graphic Proof Presentation, Proof Edition, Logical Frameworks |
42 | Myla Archer, Constance L. Heitmeyer |
Human-Style Theorem Proving Using PVS. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
40 | Karen Zee, Viktor Kuncak, Martin C. Rinard |
Full functional verification of linked data structures. |
PLDI |
2008 |
DBLP DOI BibTeX RDF |
java, verification, data structure, decision procedure, theorem prover |
40 | Sagar Chaki |
SAT-Based Software Certification. |
TACAS |
2006 |
DBLP DOI BibTeX RDF |
|
40 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Accurate Theorem Proving for Program Verification. |
ISoLA |
2004 |
DBLP DOI BibTeX RDF |
|
40 | Ingo Dahn |
Interpretation of a Mizar-Like Logic in First-Order Logic. |
FTP (LNCS Selection) |
1998 |
DBLP DOI BibTeX RDF |
|
40 | Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps. |
WoLLIC |
2007 |
DBLP DOI BibTeX RDF |
|
40 | Jan Jürjens |
Security Analysis of Crypto-based Java Programs using Automated Theorem Provers. |
ASE |
2006 |
DBLP DOI BibTeX RDF |
|
40 | Jan Jürjens |
Code Security Analysis of a Biometric Authentication System Using Automated Theorem Provers. |
ACSAC |
2005 |
DBLP DOI BibTeX RDF |
|
40 | Josef Urban |
Translating Mizar for First Order Theorem Provers. |
MKM |
2003 |
DBLP DOI BibTeX RDF |
|
40 | Marco Devillers, W. O. David Griffioen, Olaf Müller |
Possibly Infinite Sequences in Theorem Provers: A Comparative Study. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
39 | Deepak Kapur, Balakrishnan Krishnamurthy |
A Natural Proof System Based on rewriting Techniques. |
CADE |
1984 |
DBLP DOI BibTeX RDF |
|
35 | David S. Hardin, Matthew Wilding, David A. Greve |
Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
35 | D. Andre de Waal, John P. Gallagher |
The Applicability of Logic Program Analysis and Transformation to Theorem Proving. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
34 | Mark E. Stickel |
Automated theorem-proving research in the Fifth Generation Computer Systems Project: Model generation theorem provers. |
Future Gener. Comput. Syst. |
1993 |
DBLP DOI BibTeX RDF |
|
32 | Jason Hickey, Aleksey Nogin |
Fast Tactic-Based Theorem Proving. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
31 | Jasmin Christian Blanchette |
Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm. |
J. Autom. Reason. |
2009 |
DBLP DOI BibTeX RDF |
Interactive theorem provers, Huffman coding, Higher-order logic |
31 | Carl Eastlund, Matthias Felleisen |
Making induction manifest in modular ACL2. |
PPDP |
2009 |
DBLP DOI BibTeX RDF |
theorem provers, acl2, module systems |
31 | Jia Meng, Lawrence C. Paulson |
Translating Higher-Order Clauses to First-Order Clauses. |
J. Autom. Reason. |
2008 |
DBLP DOI BibTeX RDF |
Interactive theorem provers, Clause translation, First-order logic, Higher-order logic |
31 | Christian Urban |
Nominal Techniques in Isabelle/HOL. |
J. Autom. Reason. |
2008 |
DBLP DOI BibTeX RDF |
Nominal logic work, Lambda-calculus, Theorem provers |
31 | J. Santiago Jorge, Víctor M. Gulías, Laura M. Castro |
Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
Formal methods, functional programming, software verification, real-world applications, theorem provers |
31 | Carsten Fuhs, Rafael Navarro-Marset, Carsten Otto, Jürgen Giesl, Salvador Lucas, Peter Schneider-Kamp |
Search Techniques for Rational Polynomial Orders. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
Topics computer algebra systems and automated theorem provers, implementation and performance issues |
31 | Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub |
Building Decision Procedures in the Calculus of Inductive Constructions. |
CSL |
2007 |
DBLP DOI BibTeX RDF |
Calculus of Inductive Constructions, Decision procedures, Theorem provers |
31 | Frits W. Vaandrager, Adriaan de Groot |
Analysis of a biphase mark protocol with Uppaaland PVS. |
Formal Aspects Comput. |
2006 |
DBLP DOI BibTeX RDF |
Biphase mark protocol, Model checking, Formal methods, Timed automata, Theorem provers |
31 | Alexander Koller, Ralph Debusmann, Malte Gabsdil, Kristina Striegnitz |
Put My Galakmid Coin into the Dispenser and Kick It: Computational Linguistics and Theorem Proving in a Computer Game. |
J. Log. Lang. Inf. |
2004 |
DBLP DOI BibTeX RDF |
text adventures, generation, description logic, parsing, theorem provers, reference resolution, dependency grammar |
31 | Edwin D. de Jong, Jaco van de Pol, Jozef Hooman |
Refinement in Requirements Specification and Analysis: A Case Study. |
ECBS |
2000 |
DBLP DOI BibTeX RDF |
requirements specification and analysis, formal methods, refinement, theorem provers |
31 | Christine Lafontaine, Yves Ledru, Pierre-Yves Schobbens |
Two Approaches towards the Formalisation of VDM. |
VDM Europe |
1990 |
DBLP DOI BibTeX RDF |
formalisation of VDM, automated support of formal methods, theorem provers |
31 | Geoff Sutcliffe |
TPTP, TSTP, CASC, etc. |
CSR |
2007 |
DBLP DOI BibTeX RDF |
|
31 | Byron Cook, Daniel Kroening, Natasha Sharygina |
Cogent: Accurate Theorem Proving for Program Verification. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
31 | John Harrison 0001 |
Formal Verification at Intel. |
LICS |
2003 |
DBLP DOI BibTeX RDF |
|
31 | David Déharbe, Silvio Ranise |
Light-Weight Theorem Proving for Debugging and Verifying Units of Code. |
SEFM |
2003 |
DBLP DOI BibTeX RDF |
|
31 | Stephan Kepser, Jörn Richts |
UNIMOK: A System for Combining Equational Unification Algorithm. |
RTA |
1999 |
DBLP DOI BibTeX RDF |
|
31 | Dirk Fuchs |
Requirement-Based Cooperative Theorem Proving. |
JELIA |
1998 |
DBLP DOI BibTeX RDF |
|
31 | Wolfgang Ertel |
OR-Parallel Theorem Proving with Random Competition. |
LPAR |
1992 |
DBLP DOI BibTeX RDF |
random competition, SETHEO, theorem proving, speedup, OR-parallelism, random search, model elimination |
29 | Shiu-Kai Chin, Edward P. Stabler |
Synthesis of arithmetic hardware using hardware metafunctions. |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. |
1990 |
DBLP DOI BibTeX RDF |
|
27 | Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke |
LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). |
IJCAR |
2008 |
DBLP DOI BibTeX RDF |
|
27 | Renate A. Schmidt, Ullrich Hustadt |
The axiomatic translation principle for modal logic. |
ACM Trans. Comput. Log. |
2007 |
DBLP DOI BibTeX RDF |
Translation approach, small model property, completeness, decidability |
27 | Simon Colton, Stephen H. Muggleton |
Mathematical applications of inductive logic programming. |
Mach. Learn. |
2006 |
DBLP DOI BibTeX RDF |
|
27 | Jean-Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Laurent Voisin |
An Open Extensible Tool Environment for Event-B. |
ICFEM |
2006 |
DBLP DOI BibTeX RDF |
|
27 | Alessandro Armando, Luca Compagna, Silvio Ranise |
Rewriting and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation. |
Mechanizing Mathematical Reasoning |
2005 |
DBLP DOI BibTeX RDF |
|
27 | Jia Meng, Lawrence C. Paulson |
Experiments on Supporting Interactive Proof Using Resolution. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
27 | Jürgen Giesl, Armin Kühnemann, Janis Voigtländer |
Deaccumulation - Improving Provability. |
ASIAN |
2003 |
DBLP DOI BibTeX RDF |
|
27 | Anna Formica |
Finite Satisfiability of Integrity Constraints in Object-Oriented Database Schemas. |
IEEE Trans. Knowl. Data Eng. |
2002 |
DBLP DOI BibTeX RDF |
constraint satisfiability (consistency), recursive schemas, axioms of infinity, equality constraints, object-oriented databases |
27 | Andreas Meier 0002, Volker Sorge, Simon Colton |
Employing Theory Formation to Guide Proof Planning. |
AISC |
2002 |
DBLP DOI BibTeX RDF |
|
27 | Thomas Baar, Ekkart Kindler, Hagen Völzer |
Verifying Intuition - ILF Checks DAWN Proofs. |
ICATPN |
1999 |
DBLP DOI BibTeX RDF |
|
27 | Douglas J. Howe |
Interactive Theorem Proving Using Type Theory. |
CSL |
1999 |
DBLP DOI BibTeX RDF |
|
27 | Deepak Kapur, Mahadevan Subramaniam |
Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover. |
ASIAN |
1998 |
DBLP DOI BibTeX RDF |
|
27 | Dirk Fuchs |
Coupling Saturation-Based Provers by Exchanging Positive/Negative Information. |
RTA |
1998 |
DBLP DOI BibTeX RDF |
|
27 | Heribert Schütz, Tim Geisler |
Efficient Model Generation through Compilation. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
27 | Andreas Nonnengart |
Resolution-Based Calculi for Modal and Temporal Logics. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
27 | Geoff Sutcliffe, Christian B. Suttner, Theodor Yemenis |
The TPTP Problem Library. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
27 | Joe W. Duran |
Heuristics for program synthesis using loop invariants. |
ACM Annual Conference (2) |
1978 |
DBLP DOI BibTeX RDF |
Automatic programming, Program synthesis, Program correctness, Loop invariants |
26 | Mohammad Abdulaziz |
Interactive Theorem Provers: Applications in AI, Opportunities, and Challenges. |
AAAI |
2024 |
DBLP DOI BibTeX RDF |
|
26 | Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban |
A Mathematical Benchmark for Inductive Theorem Provers. |
CoRR |
2023 |
DBLP DOI BibTeX RDF |
|
26 | Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban |
A Mathematical Benchmark for Inductive Theorem Provers. |
LPAR |
2023 |
DBLP DOI BibTeX RDF |
|
26 | Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu 0010, Wenda Li, Mateja Jamnik, Guillaume Lample, Yuhuai Wu |
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. |
ICLR |
2023 |
DBLP BibTeX RDF |
|
26 | Antoine Defourné |
Encodages de la théorie des ensembles de TLA+ pour la preuve automatique. (Encoding TLA+'s Set Theory for Automated Theorem Provers). |
|
2023 |
RDF |
|
26 | Alex Kontorovich |
Foreword to: Special Issue on Interactive Theorem Provers. |
Exp. Math. |
2022 |
DBLP DOI BibTeX RDF |
|
26 | Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdz, Piotr Milos, Yuhuai Wu, Mateja Jamnik |
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|