Search results for "theorem-provers"

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