Search results for "theorem-proving"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
40	Raymond Reiter	A Semantically Guided Deductive System for Automatic Theorem Proving.	IEEE Trans. Computers	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.	CADE	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.	LPAR	2001	DBLP DOI BibTeX RDF
39	J Strother Moore	Inductive assertions and operational semantics.	Int. J. Softw. Tools Technol. Transf.	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.	Innov. Syst. Softw. Eng.	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.	J. Autom. Reason.	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.	J. Autom. Reason.	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.	SBIA	2004	DBLP DOI BibTeX RDF	planning, theorem proving, abduction, event calculus
39	Michael J. C. Gordon	Validating the PSL/Sugar Semantics Using Automated Reasoning.	Formal Aspects Comput.	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.	CADE	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.	LOPSTR	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.	ALP	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.	STACS	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.	CADE	1988	DBLP DOI BibTeX RDF	Theorem proving, set theory, term rewriting
39	Douglas J. Howe	Computational Metatheory in Nuprl.	CADE	1988	DBLP DOI BibTeX RDF	formal metamathematics, reflection, Theorem proving, type theory, constructive mathematics, tactics
38	Josef Urban	MPTP - Motivation, Implementation, First Experiments.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	ATP, Mizar, MPA, MPTP
38	Julien Schmaltz, Dominique Borrione	A functional formalization of on chip communications.	Formal Aspects Comput.	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.	J. Autom. Reason.	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.	TYPES	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.	ITP	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.	ITP	2023	DBLP DOI BibTeX RDF
37	Mario Carneiro, Chad E. Brown, Josef Urban	Automated Theorem Proving for Metamath.	ITP	2023	DBLP DOI BibTeX RDF
37	Jeremy Avigad, Assia Mahboubi	Erratum to: Interactive Theorem Proving.	ITP	2018	DBLP DOI BibTeX RDF
37	Nathan Fulton, Stefan Mitsch, Rose Bohrer, André Platzer	Bellerophon: Tactical Theorem Proving for Hybrid Systems.	ITP	2017	DBLP DOI BibTeX RDF
37	Moa Johansson	Automated Theory Exploration for Interactive Theorem Proving: - An Introduction to the Hipster System.	ITP	2017	DBLP DOI BibTeX RDF
37	Joachim Breitner	Visual Theorem Proving with the Incredible Proof Machine.	ITP	2016	DBLP DOI BibTeX RDF
37	Roderick Chapman, Florian Schanda	Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK.	ITP	2014	DBLP DOI BibTeX RDF
37	Martin Ring, Christoph Lüth	Collaborative Interactive Theorem Proving with Clide.	ITP	2014	DBLP DOI BibTeX RDF
37	Panagiotis Manolios	Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities.	ITP	2013	DBLP DOI BibTeX RDF
37	Makarius Wenzel	Shared-Memory Multiprocessing for Interactive Theorem Proving.	ITP	2013	DBLP DOI BibTeX RDF
37	K. Rustan M. Leino	Automating Theorem Proving with SMT.	ITP	2013	DBLP DOI BibTeX RDF
37	Phil Scott, Jacques D. Fleuriot	Composable Discovery Engines for Interactive Theorem Proving.	ITP	2011	DBLP DOI BibTeX RDF
37	Mike Gordon	Twenty Years of Theorem Proving for HOLs Past, Present and Future.	TPHOLs	2008	DBLP DOI BibTeX RDF
37	Lawrence C. Paulson, Kong Woei Susanto	Source-Level Proof Reconstruction for Interactive Theorem Proving.	TPHOLs	2007	DBLP DOI BibTeX RDF
37	Behzad Akbarpour, Sofiène Tahar	Error Analysis of Digital Filters Using Theorem Proving.	TPHOLs	2004	DBLP DOI BibTeX RDF
37	Silvio Ranise, David Déharbe	Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs.	FTP	2003	DBLP DOI BibTeX RDF
37	David Delahaye	Free-Style Theorem Proving.	TPHOLs	2002	DBLP DOI BibTeX RDF
37	Micaela Mayero	Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm).	TPHOLs	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.	TPHOLs	2001	DBLP DOI BibTeX RDF
37	Jason Hickey, Aleksey Nogin	Fast Tactic-Based Theorem Proving.	TPHOLs	2000	DBLP DOI BibTeX RDF
37	Don Syme	Three Tactic Theorem Proving.	TPHOLs	1999	DBLP DOI BibTeX RDF
37	Thomas Kropf	Recent Advancements in Hardware Verification - How to Make Theorem Proving Fit for an Industrial Usage.	TPHOLs	1999	DBLP DOI BibTeX RDF
37	Friedrich W. von Henke, Stephan Pfab, Holger Pfeifer, Harald Rueß	Case Studies in Meta-Level Theorem Proving.	TPHOLs	1998	DBLP DOI BibTeX RDF
37	Myla Archer, Constance L. Heitmeyer	Human-Style Theorem Proving Using PVS.	TPHOLs	1997	DBLP DOI BibTeX RDF
37	Jeremy V. Pitt, Jim Cunningham	Distributed Modal Theorem Proving with KE.	TABLEAUX	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.	TABLEAUX	1995	DBLP DOI BibTeX RDF
37	Holger Busch	First-Order Automation for Higher-Order-Logic Theorem Proving.	TPHOLs	1994	DBLP DOI BibTeX RDF
37	Richard J. Boulton	A Lazy Approach to Fully-Expansive Theorem Proving.	TPHOLs	1992	DBLP BibTeX RDF
37	Jim Cunningham, Marcello D'Agostino, Jeremy V. Pitt	Towards Tableau Theorem-Proving with Analytic Cut.	TABLEAUX	1992	DBLP BibTeX RDF
37	Vincent Risch, Camilla Schwind	Tableaux-Based Theorem Proving and Non-Standard Reasoning.	TABLEAUX	1992	DBLP BibTeX RDF
37	Zoran Ognjanovic, Dragan Urosevic, Tatjana Petrovic, Zorana Ristovic	A Tableaux Retlated Method for Modal Theorem Proving (Extended Abstract).	TABLEAUX	1992	DBLP BibTeX RDF
37	Oliver Bittel	The Lambda-Tableau Calculus: A New Approach to Theorem Proving in the Intuitionistic Logic (Extended Abstract).	TABLEAUX	1992	DBLP BibTeX RDF
37	Simon Bainbridge, Albert John Camilleri, Roger Fleming	Industrial Application of Theorem Proving to System Level Design.	TPHOLs	1991	DBLP BibTeX RDF
37	Marta Franová	Constructive Matching - A Methodology for Inductive Theorem Proving.	JELIA	1990	DBLP DOI BibTeX RDF
36	Viorica Sofronie-Stokkermans	Automated theorem proving by resolution in non-classical logics.	Ann. Math. Artif. Intell.	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.	JELIA	2004	DBLP DOI BibTeX RDF
36	Alexander V. Lyaletski, Andrey Paskevich, Konstantin Verchinine	Theorem Proving and Proof Verification in the System SAD.	MKM	2004	DBLP DOI BibTeX RDF
36	Vijay Chandru, Jean-Louis Lassez	Qualitative Theorem Proving in Linear Constraints.	Verification: Theory and Practice	2003	DBLP DOI BibTeX RDF
36	Quoc Bao Vo	A task-oriented agent-based mechanism for theorem proving.	IAT	2003	DBLP DOI BibTeX RDF
36	Gérard P. Huet	Higher Order Unification 30 Years Later.	TPHOLs	2002	DBLP DOI BibTeX RDF
36	Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov	On the Evaluation of Indexing Techniques for Theorem Proving.	IJCAR	2001	DBLP DOI BibTeX RDF
36	Steven D. Johnson	View from the Fringe of the Fringe (Joint with CHARME 2001).	TPHOLs	2001	DBLP DOI BibTeX RDF
36	Ricardo Caferra, Nicolas Peltier, François Puitg	Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization.	Automated Deduction in Geometry	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.	CADE	2000	DBLP DOI BibTeX RDF
36	Natarajan Shankar	Combining Theorem Proving and Model Checking through Symbolic Analysis.	CONCUR	2000	DBLP DOI BibTeX RDF
36	Maria Paola Bonacina	A Taxonomy of Theorem-Proving Strategies.	Artificial Intelligence Today	1999	DBLP DOI BibTeX RDF
36	Haiyan Xiong, Paul Curzon, Sofiène Tahar	Importing MDG Verification Results into HOL.	TPHOLs	1999	DBLP DOI BibTeX RDF
36	Erica Melis, Jon Whittle 0001	Internal Analogy in Theorem Proving.	CADE	1996	DBLP DOI BibTeX RDF
36	Wai Wong	Recording and Checking HOL Proofs.	TPHOLs	1995	DBLP DOI BibTeX RDF
36	Maritta Heisel, Wolfgang Reif, Werner Stephan 0001	Tactical Theorem Proving in Program Verification.	CADE	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.	SC	1990	DBLP DOI BibTeX RDF
36	Cliff B. Jones, Richard C. Moore	MUFFIN: A User Interface Design Experiment for a Theorem Proving Assistant.	VDM Europe	1988	DBLP DOI BibTeX RDF
36	Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek	Paths to High-Performance Automated Theorem Proving.	CADE	1986	DBLP DOI BibTeX RDF
36	Jieh Hsiang	Two Results in Term Rewriting Theorem Proving.	RTA	1985	DBLP DOI BibTeX RDF
35	Tomás Recio, Francisco Botana	Where the Truth Lies (in Automatic Theorem Proving in Elementary Geometry).	ICCSA (2)	2004	DBLP DOI BibTeX RDF
35	Nancy A. Day, Jeffrey J. Joyce	Symbolic Functional Evaluation.	TPHOLs	1999	DBLP DOI BibTeX RDF
35	Boutheina Chetali, Barbara Heyd	Formal Verification of Concurrent Programs in LP and in COQ: A Comparative Analysis.	TPHOLs	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.	CADE	1984	DBLP DOI BibTeX RDF
35	James R. Slagle	Automatic Theorem Proving With Renamable and Semantic Resolution.	J. ACM	1967	DBLP DOI BibTeX RDF
35	Richard J. Waldinger	Whatever Happened to Deductive Question Answering?	LPAR	2007	DBLP DOI BibTeX RDF
35	Volker Sorge, Andreas Meier 0002, Roy L. McCasland, Simon Colton	Automatic Construction and Verification of Isotopy Invariants.	J. Autom. Reason.	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.	Formal Aspects Comput.	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.	DAMP	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.	TAP	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.	PPDP	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.	Formal Aspects Comput.	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.	IFM	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.	ICTAC	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.	FATES	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.	CSL	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.	LOPSTR	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.	Int. J. Softw. Tools Technol. Transf.	2003	DBLP DOI BibTeX RDF	Formal methods, Theorem proving, Software verification
34	Stefan Blom, Jaco van de Pol	State Space Reduction by Proving Confluence.	CAV	2002	DBLP DOI BibTeX RDF	on-the-fly state space reduction, symbolic transformation, &#55CRL 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.	FME	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.	Australian Joint Conference on Artificial Intelligence	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.	Int. J. Softw. Tools Technol. Transf.	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.	IJCAR	2001	DBLP DOI BibTeX RDF	Set reasoning, map algebra, first-order theorem proving
34	Alexandre Riazanov, Andrei Voronkov	Partially Adaptive Code Trees.	JELIA	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.	FTP (LNCS Selection)	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.	CADE	1997	DBLP DOI BibTeX RDF	interactive and automatic theorem proving, atom structure, Relation algebra, Isabelle