Search results for "theorem-proving"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
27	Stéphane Fèvre, Dongming Wang 0001	Combining Algebraic Computing and Term-Rewriting for Geometry Theorem Proving.	AISC	1998	DBLP DOI BibTeX RDF
27	Mitsuharu Yamamoto, Koichi Takahashi, Masami Hagiya, Shin-ya Nishizaki, Tetsuo Tamai	Formalization of Graph Search Algorithms and Its Applications.	TPHOLs	1998	DBLP DOI BibTeX RDF
27	Ulrich Kühler, Claus-Peter Wirth	Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving.	RTA	1997	DBLP DOI BibTeX RDF
27	Albert John Camilleri	A Hybrid Approach to Verifying Liveness in a Symmetric Multi-Processor.	TPHOLs	1997	DBLP DOI BibTeX RDF
27	Vincent Zammit	A Comparative Study of Coq and HOL.	TPHOLs	1997	DBLP DOI BibTeX RDF
27	Saturnino F. Luz-Filho	Grammar Specification in Categorial Logics and Theorem Proving.	CADE	1996	DBLP DOI BibTeX RDF	Mechanisms (semantic tableaux) and Applications (computational liguistics)
27	Harald Ganzinger	Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract).	CADE	1996	DBLP DOI BibTeX RDF
27	Thomas Hillenbrand, Arnim Buch, Roland Fettig	On Gaining Efficiency in Completion-Based Theorem Proving.	RTA	1996	DBLP DOI BibTeX RDF
27	Don Syme	A New Interface for HOL - Ideas, Issues and Implementation.	TPHOLs	1995	DBLP DOI BibTeX RDF
27	E. Thomas Schubert, Sarah Mocas	A Mechanized Logic for Secure Key Escrow Protocol Verification.	TPHOLs	1995	DBLP DOI BibTeX RDF
27	David A. Plaisted	The Search Efficiency of Theorem Proving Strategies.	CADE	1994	DBLP DOI BibTeX RDF
27	Ahmed Guergueb, Jean Mainguené, Marie-Françoise Roy	Examples of Automatic Theorem Proving a Real Geometry.	ISSAC	1994	DBLP DOI BibTeX RDF
27	David A. Fura, Arun K. Somani	Interval-Semantic Component Models and the Efficient Verification of Transaction-Level Circiut Behavior.	TPHOLs	1994	DBLP DOI BibTeX RDF
27	Mats Larsson	An Engineering Approach to Formal Digital System Design.	TPHOLs	1994	DBLP DOI BibTeX RDF
27	Ching-Tsun Chou	Mechanical Verification of Distributed Algorithms in Higher-Order Logic.	TPHOLs	1994	DBLP DOI BibTeX RDF
27	Phillip J. Windley	Specifying Instruction-Set Architectures in HOL: A Primer.	TPHOLs	1994	DBLP DOI BibTeX RDF
27	Marta Franová, Yves Kodratoff, Martine Gross	Constructive Matching Methodology: Formally Creative or Intelligent Inductive Theorem Proving?	ISMIS	1993	DBLP DOI BibTeX RDF
27	Jürgen Avenhaus, Jörg Denzinger	Distributing Equational Theorem Proving.	RTA	1993	DBLP DOI BibTeX RDF
27	Zheng Zhu, Jeffrey J. Joyce, Carl-Johan H. Seger	Verification of the Tamarack-3 Microprocessor in a Hybrid Verification Environment.	HUG	1993	DBLP DOI BibTeX RDF
27	Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi	TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory.	HUG	1993	DBLP DOI BibTeX RDF
27	Catia M. Angelo, Luc J. M. Claesen, Hugo De Man	Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL.	HUG	1993	DBLP DOI BibTeX RDF
27	Newton C. A. da Costa, Lawrence J. Henschen, James J. Lu, V. S. Subrahmanian	Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation.	CADE	1990	DBLP DOI BibTeX RDF
27	Christoph Walther	Many-Sorted Inferences in Automated Theorem Proving.	Sorts and Types in Artificial Intelligence	1989	DBLP DOI BibTeX RDF
27	Larry M. Hines	Hyper-Chaining and Knowledge-Based Theorem Proving.	CADE	1988	DBLP DOI BibTeX RDF
27	John K. Dixon	Z-Resolution: Theorem-Proving with Compiled Axioms.	J. ACM	1973	DBLP DOI BibTeX RDF
26	Kenichi Yajima, Shoichi Morimoto, Daisuke Horie, Noor Sheila Azreen, Yuichi Goto, Jingde Cheng	FORVEST: A Support Tool for Formal Verification of Security Specifications with ISO/IEC 15408.	ARES	2009	DBLP DOI BibTeX RDF
26	John M. Rushby	Harnessing Disruptive Innovation in Formal Verification.	SEFM	2006	DBLP DOI BibTeX RDF
26	Julian Richardson	A Semantics for Proof Plans with Applications to Interactive Proof Planning.	LPAR	2002	DBLP DOI BibTeX RDF
26	Manfred Kerber, Martin Pollet	On the Design of Mathematical Concepts.	Australian Joint Conference on Artificial Intelligence	2002	DBLP DOI BibTeX RDF
26	Constance L. Heitmeyer	On the Need for Practical Formal Methods.	FTRTFT	1998	DBLP DOI BibTeX RDF
26	Robert Matzinger	Computational Representations of Herbrand Models Using Grammars.	CSL	1996	DBLP DOI BibTeX RDF
26	Ken Hirose	An Approach to Proof Checker.	MFCS	1986	DBLP DOI BibTeX RDF
26	Nicola Olivetti, Gian Luca Pozzato	Nested sequent calculi and theorem proving for normal conditional logics: The theorem prover NESCOND.	Intelligenza Artificiale	2015	DBLP DOI BibTeX RDF
26	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
25	Edwin C. Brady	Ivor, a Proof Engine.	IFL	2006	DBLP DOI BibTeX RDF
25	Tarek Mhamdi, Sofiène Tahar	Providing Automated Verification in HOL Using MDGs.	ATVA	2004	DBLP DOI BibTeX RDF
25	Andrei Voronkov	Algorithms, Datastructures, and other Issues in Efficient Automated Deduction.	IJCAR	2001	DBLP DOI BibTeX RDF
25	Christoph Lüth, Burkhart Wolff	More About TAS and IsaWin - Tools for Formal Program Development.	FASE	2000	DBLP DOI BibTeX RDF
24	Deepak Kapur, Balakrishnan Krishnamurthy	A Natural Proof System Based on rewriting Techniques.	CADE	1984	DBLP DOI BibTeX RDF
24	Lawrence J. Henschen, Larry Wos	Unit Refutations and Horn Sets.	J. ACM	1974	DBLP DOI BibTeX RDF
22	Myla Archer, Hongping Lim, Nancy A. Lynch, Sayan Mitra, Shinya Umeno	Specifying and proving properties of timed I/O automata in the TIOA toolkit.	MEMOCODE	2006	DBLP DOI BibTeX RDF
22	Ralph D. Jeffords, Constance L. Heitmeyer	A strategy for efficiently verifying requirements.	ESEC / SIGSOFT FSE	2003	DBLP DOI BibTeX RDF	model checking, formal methods, software tools, invariants, requirements specification, compositional verification
21	Warren A. Hunt Jr., Sol Swords	Centaur Technology Media Unit Verification.	CAV	2009	DBLP DOI BibTeX RDF
21	Timothy L. Hinrichs	Extensional Reasoning.	SARA	2007	DBLP DOI BibTeX RDF
21	Xia Wu, Jigui Sun, Kun Hou	An Extension Rule Based First-Order Theorem Prover.	KSEM	2006	DBLP DOI BibTeX RDF
21	John M. Rushby	Tutorial: Automated Formal Methods with PVS, SAL, and Yices.	SEFM	2006	DBLP DOI BibTeX RDF
21	Stefano Brait, Franco Fummi, Graziano Pravadelli	On the use of a high-level fault model to analyze logical consequence of properties.	MEMOCODE	2005	DBLP DOI BibTeX RDF
21	Thomas Raths, Jens Otten, Christoph Kreitz	The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic.	TABLEAUX	2005	DBLP DOI BibTeX RDF
21	Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber	Can a Higher-Order and a First-Order Theorem Prover Cooperate?.	LPAR	2004	DBLP DOI BibTeX RDF
21	Ullrich Hustadt, Boris Motik, Ulrike Sattler	A Decomposition Rule for Decision Procedures by Resolution-Based Calculi.	LPAR	2004	DBLP DOI BibTeX RDF
21	Vu Ha, Murali Rangarajan, Darren D. Cofer, Harald Rueß, Bruno Dutertre	Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software: An Experience Report.	ICSE	2004	DBLP DOI BibTeX RDF
21	Konstantine Arkoudas, Selmer Bringsjord	Metareasoning for Multi-agent Epistemic Logics.	CLIMA	2004	DBLP DOI BibTeX RDF
21	Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth	How to Prove Inductive Theorems? QUODLIBET!	CADE	2003	DBLP DOI BibTeX RDF
21	Steve Roach, Jeffrey Van Baalen	Experience Report on Automated Procedure Construction for Deductive Synthesis.	ASE	2002	DBLP DOI BibTeX RDF
21	V. K. Pisini, Sofiène Tahar, Paul Curzon, Otmane Aït Mohamed, Xiaoyu Song	Formal hardware verification by integrating HOL and MDG.	ACM Great Lakes Symposium on VLSI	2000	DBLP DOI BibTeX RDF
21	Ingo Dahn	Interpretation of a Mizar-Like Logic in First-Order Logic.	FTP (LNCS Selection)	1998	DBLP DOI BibTeX RDF
21	Gilles Défourneaux, Nicolas Peltier	Partial Matching for Analogy Discovery in Proofs and Counter-Examples.	CADE	1997	DBLP DOI BibTeX RDF
21	Koji Iwanuma	Lemma Matching for a PTTP-based Top-down Theorem Prover.	CADE	1997	DBLP DOI BibTeX RDF
21	Alan M. Frisch, Richard B. Scherl	A Constraint Logic Approach to Modal Deduction.	JELIA	1990	DBLP DOI BibTeX RDF
21	David A. Schmidt	A Programming Notation for Tactical Reasoning.	CADE	1984	DBLP DOI BibTeX RDF
21	Petros Papapanagiotou, Jacques D. Fleuriot	Formal Verification of Web Services Composition Using Linear Logic and the pi-calculus.	ECOWS	2011	DBLP DOI BibTeX RDF	proofs-as-processes, Web Services, formal verification, theorem proving, services composition
21	Hui Kong 0004, Hehua Zhang, Xiaoyu Song, Ming Gu 0001, Jiaguang Sun 0001	Proving Computational Geometry Algorithms in TLA+2.	TASE	2011	DBLP DOI BibTeX RDF	algorithm verification, TLA+2, geometry algorithm, theorem proving, loop invariant
21	Florian Haftmann	From higher-order logic to Haskell: there and back again.	PEPM	2010	DBLP DOI BibTeX RDF	code generation, theorem proving, haskell, higher-order logic, isabelle
21	Sander Vermolen, Jozef Hooman, Peter Gorm Larsen	Proving consistency of VDM models using HOL.	SAC	2010	DBLP DOI BibTeX RDF	verification, theorem proving, VDM, HOL, model consistency
21	Tuan Minh Pham	Similar triangles and orientation in plane elementary geometry for Coq-based proofs.	SAC	2010	DBLP DOI BibTeX RDF	similar triangles, orientation, formalization, Coq, geometric theorem proving
21	Simon Meier, Cas Cremers, David A. Basin	Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs.	CSF	2010	DBLP DOI BibTeX RDF	formal methods, theorem proving, security protocols, automatic tools
21	Asma Moubaiddin, Nadim Obeid	Partial information basis for agent-based collaborative dialogue.	Appl. Intell.	2009	DBLP DOI BibTeX RDF	Partial information states, Agent, Theorem proving, Argument, Dialogue, Three-valued logic, Nonmonotonic
21	Giorgio Dalzotto, Tomás Recio	On Protocols for the Automated Discovery of Theorems in Elementary Geometry.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Automatic theorem discovery, Elementary geometry, Computational algebraic geometry, Automatic theorem proving
21	Magnus Björk	First Order Stålmarck.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Stålmarck’s method, Universal lemmas, First order logic, Automated theorem proving, Intersections
21	Harvey Tuch	Formal Verification of C Systems Code.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	C, Separation logic, Interactive theorem proving
21	Matthias Daum 0001, Jan Dörrenbächer, Burkhart Wolff	Proving Fairness and Implementation Correctness of a Microkernel Scheduler.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Formal verification, Interactive theorem proving, Microkernel, Isabelle/HOL
21	Marcel Oliveira, Ana Cavalcanti 0001, Jim Woodcock 0001	A UTP semantics for Circus.	Formal Aspects Comput.	2009	DBLP DOI BibTeX RDF	Concurrency, Theorem proving, Relational model, Refinement calculus
21	Jens Bendisposto, Michael Leuschel	Proof Assisted Model Checking for B.	ICFEM	2009	DBLP DOI BibTeX RDF	Model Checking, Experiment, Theorem Proving, B-Method, Tool Integration
21	André Platzer, Jan-David Quesel	European Train Control System: A Case Study in Formal Verification.	ICFEM	2009	DBLP DOI BibTeX RDF	formal verification of hybrid systems, train control, parameter constraint identification, theorem proving, disturbances
21	Faranak Heidarian, Julien Schmaltz, Frits W. Vaandrager	Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks.	FM	2009	DBLP DOI BibTeX RDF	wireless sensor networks, model checking, theorem proving, timed automata, clock synchronization, industrial application
21	Levent Erkök, John Matthews	Pragmatic equivalence and safety checking in Cryptol.	PLPV	2009	DBLP DOI BibTeX RDF	sat/smt solving, size polymorphism, formal methods, cryptography, theorem proving, equivalence checking
21	Amy P. Felty, Alberto Momigliano	Reasoning with hypothetical judgments and open terms in hybrid.	PPDP	2009	DBLP DOI BibTeX RDF	name-binding, induction, logical frameworks, higher-order abstract syntax, interactive theorem proving
21	Xiaolei Gao, Huaikou Miao	Proving Total Correctness of Refinement Based on Tableau.	ISPA	2009	DBLP DOI BibTeX RDF	Tableau method, Specification, refinement, theorem proving, Program Synthesis, total correctness
21	Jorge F. Salas	A Language for Encoding and Reconstruction of Rewriting Proofs.	SCCC	2009	DBLP DOI BibTeX RDF	Semiautomated theorem proving, encoding languages for proofs, rewriting induction, rewriting systems
21	Achim D. Brucker, Burkhart Wolff	hol-TestGen.	FASE	2009	DBLP DOI BibTeX RDF	symbolic test-case generations, theorem proving, black box testing, white box testing, interactive testing
21	Helmut Seidl, Kumar Neeraj Verma	Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying.	ACM Trans. Comput. Log.	2008	DBLP DOI BibTeX RDF	instantiation-based theorem proving, Cryptographic protocols, first-order logic, resolution, Horn clauses
21	Susanne Graf	OMEGA: correct development of real time and embedded systems.	Softw. Syst. Model.	2008	DBLP DOI BibTeX RDF	Support for object oriented, Component-based system design, Model checking, UML, Embedded systems, Real time, Theorem proving, Type-checking, Model-based
21	Marc Bezem, Dimitri Hendriks	On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Coherent logic, Proof objects, Hessenberg’s theorem, Automated theorem proving
21	Achim D. Brucker, Burkhart Wolff	An Extensible Encoding of Object-oriented Data Models in hol.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Verification, Theorem proving, Object-oriented data models, hol
21	Sandip Ray, Warren A. Hunt Jr., John Matthews, J Strother Moore	A Mechanical Analysis of Program Verification Strategies.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Inductive assertions, Partial correctness, Theorem proving, Invariants, Total correctness
21	Hasan Amjad	Data Compression for Proof Replay.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Proof translation, Interactive theorem proving, SAT solvers
21	André Platzer	Differential Dynamic Logic for Hybrid Systems.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Verification of hybrid systems, Differential equations, Automated theorem proving, Dynamic logic, Sequent calculus, Axiomatisation
21	Asem Kasem, Tetsuo Ida	Computational origami environment on the web.	Frontiers Comput. Sci. China	2008	DBLP DOI BibTeX RDF	computational origami, symbolic web services, origami theorem proving, symbolic computation
21	Leo Freitas, Jim Woodcock 0001	Mechanising Mondex with Z/Eves.	Formal Aspects Comput.	2008	DBLP DOI BibTeX RDF	Electronic finance, Grand Challenge in Verified Software, Software archaeology, Z/Eves, Security, Verification, Refinement, Theorem proving, Smart cards, Correctness, Z notation, Grand challenges, Verified Software Repository, Mondex
21	Jim Woodcock 0001, Susan Stepney, David Cooper, John A. Clark, Jeremy Jacob	The certification of the Mondex electronic purse to ITSEC Level E6.	Formal Aspects Comput.	2008	DBLP DOI BibTeX RDF	Electronic finance, Grand Challenge in Verified Software, ITSEC Level E6, Security, Verification, Refinement, Theorem proving, Smart cards, Certification, Correctness, Z notation, Grand challenges, Verified Software Repository, Mondex
21	Florian Kammüller	Formalizing non-interference for a simple bytecode language in Coq.	Formal Aspects Comput.	2008	DBLP DOI BibTeX RDF	Formal methods for security, Programming language analysis, Interactive theorem proving, Modular specification
21	Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif	Automating Algebraic Specifications of Non-freely Generated Data Types.	ATVA	2008	DBLP DOI BibTeX RDF	SAT checking, theorem proving, first-order logic, abstract data types, Algebraic specifications, finite models
21	Dominique Borrione, Amr Helmy, Laurence Pierre, Julien Schmaltz	Executable formal specification and validation of NoC communication infrastructures.	SBCCI	2008	DBLP DOI BibTeX RDF	simulation, verification, theorem proving
21	Ewen Denney, Bernd Fischer 0002	Generating customized verifiers for automatically generated code.	GPCE	2008	DBLP DOI BibTeX RDF	logical annotations, program verification, automated theorem proving, hoare logic, software certification, automated code generation
21	Wendy Verbruggen, Edsko de Vries, Arthur Hughes	Polytypic programming in COQ.	ICFP-WGP	2008	DBLP DOI BibTeX RDF	kind-indexed types, theorem proving, generic programming, formalization, coq, polytypic programming
21	Alexander Krauss 0001	Pattern minimization problems over recursive data types.	ICFP	2008	DBLP DOI BibTeX RDF	complexity, pattern matching, theorem proving
21	André Platzer, Jan-David Quesel	KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description).	IJCAR	2008	DBLP DOI BibTeX RDF	verification of hybrid systems, decision procedures, computer algebra, automated theorem proving, dynamic logic
21	John Derrick, Gerhard Schellhorn, Heike Wehrheim	Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack.	FMOODS	2008	DBLP DOI BibTeX RDF	non-atomic refinement, KIV, refinement, theorem proving, Z, linearizability, concurrent access
21	Chunqing Chen, Jin Song Dong, Jun Sun 0001	A verification system for timed interval calculus.	ICSE	2008	DBLP DOI BibTeX RDF	real-time systems, theorem proving, specification language, pvs
21	Lucas Dixon, Ross Duncan	Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF	categorical logic, graphical calculi, quantum computing, graph rewriting, interactive theorem proving