Search results for "theorem prover"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Raul H. C. Lopes, Mark Tarver	Inducing Theorem Provers from Proofs. (PDF / PS)	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
3	Stefan Gerberding	DT - An Automated Theorem Prover for Multiple-Valued First-Order Predicate Logics. (PDF / PS)	ISMVL	1996	DBLP DOI BibTeX RDF	Deep Thought, multiple-valued first-order logics, lemma generation, tableau expansion, branch closure, theorem proving, multivalued logic, multiple-valued logics, quantifiers, first-order predicate logic, truth tables, automated theorem prover
3	Anand Chavan, Shiu-Kai Chin, Shahid Ikram, Jang Dae Kim, Juin-Yeu Zu	Extending VLSI design with higher-order logic. (PDF / PS)	ICCD	1995	DBLP DOI BibTeX RDF	Cambridge Higher-Order Logic theorem-prover, microprogram sequencer, Am2910, VLSI, formal verification, formal verification, logic testing, theorem proving, logic design, logic CAD, VLSI design, higher-order logic, theorem-prover, design environment, instruction-set architecture, VLSI CAD
3	D. Sarkar, S. C. De Sarkar	A Theorem Prover for Verifying Iterative Programs Over Integers.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	rule-based theorem prover, iterative programs, overall proof construction strategy, array-sorting program, expert systems, theorem proving, program verification, performance measures, iterative methods, correctness proofs
2	Sa'ed Abed, Otmane Aït Mohamed	MDGs Reduction Technique Based on the HOL Theorem Prover.	ISMVL	2010	DBLP DOI BibTeX RDF	Soundness, Reduction Techniques, Multiway Decision Graphs, HOL Theorem Prover
2	Mahadevan Subramaniam, Ling Xiao, Bo Guo, Zoltán Pap	An Approach for Test Selection for EFSMs Using a Theorem Prover.	TestCom/FATES	2009	DBLP DOI BibTeX RDF
2	Laura Kovács, Andrei Voronkov	Finding Loop Invariants for Programs over Arrays Using a Theorem Prover.	FASE	2009	DBLP DOI BibTeX RDF
2	Dru McCandless, Leo Obrst, Shayn Hawthorne	Dynamic Web Service Assembly Using OWL and a Theorem Prover.	ICSC	2009	DBLP DOI BibTeX RDF
2	Osman Hasan, Sofiène Tahar	Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Real-time systems, Communication protocols, Higher-order-logic, Probability theory, HOL theorem prover
2	Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane	An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs.	J. Comput. Sci. Technol.	2009	DBLP DOI BibTeX RDF	correctness, reachability analysis, multiway decision graphs, HOL theorem prover
2	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
2	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
2	Konstantin Korovin	iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description).	IJCAR	2008	DBLP DOI BibTeX RDF
2	Osman Hasan, Sofiène Tahar	Performance Analysis of ARQ Protocols using a Theorem Prover.	ISPASS	2008	DBLP DOI BibTeX RDF
2	Joseph P. Near, William E. Byrd, Daniel P. Friedman	alpha-leanTAP: A Declarative Theorem Prover for First-Order Classical Logic.	ICLP	2008	DBLP DOI BibTeX RDF
2	Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane	Reachability analysis using multiway decision graphs in the HOL theorem prover.	SAC	2008	DBLP DOI BibTeX RDF	reachability analysis, HOL, multiway decision graphs
2	Aaron R. Coble	Formalized Information-Theoretic Proofs of Privacy Using the HOL4 Theorem-Prover.	Privacy Enhancing Technologies	2008	DBLP DOI BibTeX RDF
2	Osman Hasan, Sofiène Tahar	Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Coupon collector’s problem, Probabilistic analysis, Higher-order-logic, Probability theory, Statistical properties, HOL theorem prover
2	Nicola Olivetti, Gian Luca Pozzato, Camilla Schwind	A sequent calculus and a theorem prover for standard conditional logics.	ACM Trans. Comput. Log.	2007	DBLP DOI BibTeX RDF	Analytic sequent calculi, labeled deductive systems, logic programming, proof theory, automated deduction, conditional logics
2	Richard Bonichon, David Delahaye, Damien Doligez	Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs.	LPAR	2007	DBLP DOI BibTeX RDF
2	Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato	An Implementation of a Free-Variable Tableaux for KLM Preferential Logic P of Nonmonotonic Reasoning: The Theorem Prover FreeP 1.0.	AI*IA	2007	DBLP DOI BibTeX RDF
2	Laura Giordano, Valentina Gliozzi, Gian Luca Pozzato	KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning.	TABLEAUX	2007	DBLP DOI BibTeX RDF
2	Abdessamad Imine, Michaël Rusinowitch	Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms.	Rewriting, Computation and Proof	2007	DBLP DOI BibTeX RDF
2	Julien Narboux	A Graphical User Interface for Formal Proofs in Geometry.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Interface, Geometry, Automated theorem proving, Theorem prover, Proof assistant, Coq, Dynamic geometry
2	Tadashi Takahashi, Hidetsune Kobayashi	The Effect of the Theorem Prover in Cognitive Science.	International Conference on Computational Science	2006	DBLP DOI BibTeX RDF
2	Jun Sawada, Erik Reeber	ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool.	FMCAD	2006	DBLP DOI BibTeX RDF
2	Xia Wu, Jigui Sun, Kun Hou	An Extension Rule Based First-Order Theorem Prover.	KSEM	2006	DBLP DOI BibTeX RDF
2	Shinya Umeno, Nancy A. Lynch	Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study.	FM	2006	DBLP DOI BibTeX RDF
2	Ian Horrocks, Andrei Voronkov	Reasoning Support for Expressive Ontology Languages Using a Theorem Prover.	FoIKS	2006	DBLP DOI BibTeX RDF
2	Kenneth Roe	The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover.	CAV	2006	DBLP DOI BibTeX RDF
2	Erik Reeber, Jun Sawada	Combining ACL2 and an automated verification tool to verify a multiplier.	ACL2	2006	DBLP DOI BibTeX RDF	model checking, theorem proving, hardware verification
2	Julien Schmaltz, Dominique Borrione	Towards a formal theory of on chip communications in the ACL2 logic.	ACL2	2006	DBLP DOI BibTeX RDF	formal theory, network on a chip, theorem proving, communication theory
2	Dale Vaillancourt, Rex L. Page, Matthias Felleisen	ACL2 in DrScheme.	ACL2	2006	DBLP DOI BibTeX RDF	DrScheme, TeachScheme!, formal methods, pedagogy, ACL2
2	Greta Yorsh, Thomas Ball, Mooly Sagiv	Testing, abstraction, theorem proving: better together!	ISSTA	2006	DBLP DOI BibTeX RDF	fabricated states, state-based coverage, testing, abstraction, program analysis, abstract interpretation, coverage, theorem prover, software fault injection, adequacy criteria
2	Marcel Oliveira, Ana Cavalcanti, Jim Woodcock	Unifying Theories in ProofPower-Z.	UTP	2006	DBLP DOI BibTeX RDF	Unifying Theories of Programming, theorem prover
2	Kaustuv Chaudhuri, Frank Pfenning	A Focusing Inverse Method Theorem Prover for First-Order Linear Logic.	CADE	2005	DBLP DOI BibTeX RDF
2	Yoshinao Isobe, Markus Roggenbach	A Generic Theorem Prover of CSP Refinement.	TACAS	2005	DBLP DOI BibTeX RDF
2	Mizuhito Ogawa, Eiichi Horita, Satoshi Ono	Proving Properties of Incremental Merkle Trees.	CADE	2005	DBLP DOI BibTeX RDF	temporal authentication, theorem prover, Merkle tree
2	Kun Wei, James Heather	Embedding the Stable Failures Model of CSP in PVS.	IFM	2005	DBLP DOI BibTeX RDF	CSP, deadlock, determinism, liveness, theorem prover
2	Noboru Matsuda, Kurt VanLehn	GRAMY: A Geometry Theorem Prover Capable of Construction.	J. Autom. Reasoning	2004	DBLP DOI BibTeX RDF	automated geometry theorem proving, search control, intelligent tutoring system, constraint satisfaction problem, construction
2	Daniel Winterstein, Alan Bundy, Corin A. Gurr	Dr.Doodle: A Diagrammatic Theorem Prover.	IJCAR	2004	DBLP DOI BibTeX RDF
2	Kenneth L. McMillan	An Interpolating Theorem Prover.	TACAS	2004	DBLP DOI BibTeX RDF
2	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
2	Hasan Amjad	Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover.	TPHOLs	2003	DBLP DOI BibTeX RDF
2	Nicola Olivetti, Gian Luca Pozzato	CondLean: A Theorem Prover for Conditional Logics.	TABLEAUX	2003	DBLP DOI BibTeX RDF
2	Viktor K. Sabelfeld, Kai Kapp	Numeric Types in Formal Synthesis.	Ershov Memorial Conference	2003	DBLP DOI BibTeX RDF	correct hardware synthesis, formal specification, higher-order logic, theorem prover, arithmetic operations
2	Hugh Anderson	Abstract Interpretation with a Theorem Prover.	ICFEM	2002	DBLP DOI BibTeX RDF
2	Virginie Thion, Serenella Cerrito, Marta Cialdea Mayer	A General Theorem Prover for Quantified Modal Logics.	TABLEAUX	2002	DBLP DOI BibTeX RDF
2	Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Yasuyuki Shirai	A Model Generation Based Theorem Prover MGTP for First-Order Logic.	Computational Logic: Logic Programming and Beyond	2002	DBLP DOI BibTeX RDF
2	Reinhold Letz, Gernot Stenz	DCTP - A Disconnection Calculus Theorem Prover - System Abstract.	IJCAR	2001	DBLP DOI BibTeX RDF
2	Dominique Pastre	MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction.	IJCAR	2001	DBLP DOI BibTeX RDF
2	Joshua S. Hodas, Naoyuki Tamura	lolliCop - A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic.	IJCAR	2001	DBLP DOI BibTeX RDF
2	Jens Happe	The MODPROF Theorem Prover.	IJCAR	2001	DBLP DOI BibTeX RDF
2	Michael Beeson	A Second-Order Theorem Prover Applied to Circumscription.	IJCAR	2001	DBLP DOI BibTeX RDF
2	Matt Kaufmann	Verification of Year 2000 conversion rules using the ACL2 theorem prover.	STTT	2000	DBLP DOI BibTeX RDF	Formal verification, Program transformation, Automated reasoning, ACL2, Year 2000
2	George C. Necula, Peter Lee	Proof Generation in the Touchstone Theorem Prover.	CADE	2000	DBLP DOI BibTeX RDF
2	Carsten Sinz	System Description: ARA - An Automatic Theorem Prover for Relation Algebras.	CADE	2000	DBLP DOI BibTeX RDF
2	Martin Hofmann, Francis Tang	Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover.	TPHOLs	2000	DBLP DOI BibTeX RDF
2	José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos	Formalizing Rewriting in the ACL2 Theorem Prover.	AISC	2000	DBLP DOI BibTeX RDF
2	Padmanabhan Krishnan	Consistency checks for UML.	APSEC	2000	DBLP DOI BibTeX RDF	UML consistency checking, state predicates, PVS theorem prover, Prototype Verification System, partially specified systems, behavioural description, Unified Modeling Language, formal verification, theorem proving, specification languages, diagrams, computation history, UML diagrams, dynamic aspects
2	David Spelt, Susan Even	A Theorem Prover-Based Analysis Tool for Object-Oriented Databases.	TACAS	1999	DBLP DOI BibTeX RDF
2	Gernot Stenz, Andreas Wolf	E-SETHEO: Design, Configuration and Use of a Parallel Automated Theorem Prover.	Australian Joint Conference on Artificial Intelligence	1999	DBLP DOI BibTeX RDF
2	Paul Z. Kolano	Proof Assistance for Real-Time Systems Using an Interactive Theorem Prover.	ARTS	1999	DBLP DOI BibTeX RDF
2	Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt	System Description: card TAP: The First Theorem Prover on a Smart Card.	CADE	1998	DBLP BibTeX RDF
2	Yves Ledru	Identifying Pre-Conditions with the Z/EVES Theorem Prover. (PDF / PS)	ASE	1998	DBLP DOI BibTeX RDF
2	Deepak Kapur, Mahadevan Subramaniam	Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover.	ASIAN	1998	DBLP DOI BibTeX RDF
2	Karsten Konrad	HOT: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux.	TPHOLs	1998	DBLP DOI BibTeX RDF
2	David 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
2	Christian Blumenröhr, Dirk Eisenbiegler	Performing High-Level Synthesis via Program Transformations within a Theorem Prover.	EUROMICRO	1998	DBLP DOI BibTeX RDF
2	Boutheina Chetali	Formal Verification of Concurrent Programs Using the Larch Prover.	IEEE Trans. Software Eng.	1998	DBLP DOI BibTeX RDF	theorem prover methodology, Larch prover, computer-checked proof, Formal verification, communication protocol, protocol verification, UNITY
2	Koji Iwanuma	Lemma Matching for a PTTP-based Top-down Theorem Prover.	CADE	1997	DBLP DOI BibTeX RDF
2	Maria Paola Bonacina	The Clause-Diffusion Theorem Prover Peers-mcd (System Description).	CADE	1997	DBLP DOI BibTeX RDF
2	John K. Slaney	Minlog: A Minimal Logic Theorem Prover.	CADE	1997	DBLP DOI BibTeX RDF
2	Sten Agerholm, Jacob Frost	An Isabelle-Based Theorem Prover for VDM-SL.	TPHOLs	1997	DBLP DOI BibTeX RDF
2	Keith Vanderveen, C. V. Ramamoorthy	Partial instantiation theorem proving for distributed resource location. (PDF / PS)	COMPSAC	1997	DBLP DOI BibTeX RDF	partial instantiation theorem prover, distributed resource location, INSTANT, clausal form, non clausal form, GSAT algorithm, propositional sentence, request matching, CORBA Object Trading Service, KIF, theorem proving, satisfiability, first order logic, KQML
2	Dieter Fensel, Arno Schönegge	Using KIV to Specify and Verify Architectures of Knowledge-Based Systems. (PDF / PS)	ASE	1997	DBLP DOI BibTeX RDF	reusable elements, Karlsruhe interactive verifier, algorithmic specification, interactive theorem prover, proof management, proof reuse, formal specification, formal specifications, knowledge-based systems, specification language, abstract data types, dynamic logic, functional specification
2	Savi Maharaj, Juan Bicarregui	On the Verification of VDM Specification and Refinement with PVS. (PDF / PS)	ASE	1997	DBLP DOI BibTeX RDF	VDM specification, VDM formal method, PVS theorem prover, VDM-SL specification translation, PVS specification language, transparent translation methods, specification type-checking, nontrivial validation conditions, abstract specification, shallow embedding technique, verification, formal specification, proof rules
2	Johann Schumann, Bernd Fischer 0002	NORA/HAMMR: Making Deduction-Based Software Component Retrieval Practical. (PDF / PS)	ASE	1997	DBLP DOI BibTeX RDF	deduction-based software component retrieval, NORA/HAMMR, search keys, proof tasks, rejection filters, model checking techniques, confirmation filter, software reusability, signature matching, automated theorem prover
2	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
2	Tanel Tammet	A Resolution Theorem Prover for Intuitonistic Logic.	CADE	1996	DBLP DOI BibTeX RDF
2	Torsten Schaub, Stefan Brüning, Pascal Nicolas	XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description.	CADE	1996	DBLP DOI BibTeX RDF
2	Yves Ledru	Using KIDS as a Tool Support for VDM.	ICSE	1996	DBLP BibTeX RDF	KIDS, REGROUP, VDM specifications, correctness preserving transformations, executable prototypes synthesis, proof of consistency, formal specification, REFINE, theorem proving, program verification, specification languages, tool support, theorem prover, VDM
2	Pierre Bieber	Formal Techniques for an ITSEC-E4 Secure Gateway.	ACSAC	1996	DBLP DOI BibTeX RDF	ITSEC-E4 secure gateway, interactive theorem prover, Information Technology Security Evaluation Criteria, formal specification, security policy, security architecture, formal technique, functional specifications
2	Randall W. Lichota, Grace L. Hammonds, Stephen H. Brackin	Verifying The Correctness Of Cryptographic Protocols Using "Convince".	ACSAC	1996	DBLP DOI BibTeX RDF	Convince, theorem proving component, commercial computer aided software engineering tool, StP/OMT, textual notations, Higher Order Logic theorem prover, protocols, cryptographic protocols, authentication protocols, front-end, belief logic, correctness verification, automated support
2	Scott Hazelhurst, Carl-Johan H. Seger	A simple theorem prover based on symbolic trajectory evaluation and BDD's.	IEEE Trans. on CAD of Integrated Circuits and Systems	1995	DBLP DOI BibTeX RDF
2	Holger Busch	A Practical Method for Reasoning about Distributed Systems in a Theorem Prover.	TPHOLs	1995	DBLP DOI BibTeX RDF
2	David Cyrluk, Mandayam K. Srivas	Theorem proving: not an esoteric diversion, but the unifying framework for industrial verification. (PDF / PS)	ICCD	1995	DBLP DOI BibTeX RDF	industrial hardware verification, industrial verification, formal verification, logic testing, theorem proving, theorem prover, hardware verification
2	Milica Barjaktarovic, Shiu-Kai Chin, Kamal Jabbour	Formal specification and verification of communication protocols using automated tools .	ICECCS	1995	DBLP DOI BibTeX RDF	OSI protocol, large models, simulation, modelling, formal specification, formal specification, testing, protocols, formal verification, software tools, validation, theorem proving, process algebra, communication protocols, open systems, algebra, formal logic, automated tools, model checker, model testing, complex models, automated theorem prover
2	Wendy MacCaull	Finite Algebraic Models for Residuated Logic. (PDF / PS)	ISMVL	1995	DBLP DOI BibTeX RDF	finite algebraic models, residuated logic, model pruning, nonclassical logics, combinatorial explosions, structure theorems, residuated algebras, theorem proving, inference mechanisms, search problems, multivalued logic, approximate reasoning, substructural logics, algebraic semantics, automated theorem prover
2	Ramayya Kumar, Thomas Kropf, Klaus Schneider	Formal synthesis of circuits with a simple handshake protocol.	VLSI Design	1995	DBLP DOI BibTeX RDF	formal circuit synthesis, preproven building blocks, higher-order temporal operators, parametrized data signals, sequentially composed modules, parallel module composition, protocols, high level synthesis, logic design, operator semantics, template, formal logic, correctness proofs, synchronous circuits, handshake protocol, HOL theorem prover
2	David R. Lester, Sava Mintchev	Towards Machine-Checked Compiler Correctness for Higher-order Pure Functional Languages.	CSL	1994	DBLP DOI BibTeX RDF	Congruence Proof, Lambda Calculus, Denotational Semantics, Theorem Prover, Compiler Correctness
2	George K. Papakonstantinou, T. Panayiotopoulos	A full theorem-prover under uncertainty.	Journal of Intelligent and Robotic Systems	1993	DBLP DOI BibTeX RDF	inexact reasoning, Prolog, theorem-proving, certainty, model elimination
2	John Harrison, Laurent Théry	Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals.	HUG	1993	DBLP DOI BibTeX RDF
2	Jeffrey J. Joyce, Carl-Johan H. Seger	The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover.	HUG	1993	DBLP DOI BibTeX RDF
2	Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita	MGTP: A Parallel Theorem Prover Based on Lazy Model Generation.	CADE	1992	DBLP DOI BibTeX RDF
2	Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa	Embedding Negation as Failure into a Model Generation Theorem Prover.	CADE	1992	DBLP DOI BibTeX RDF
2	Ulrich Fraus, Heinrich Hußmann	An Inductive Theorem Prover Based on Narrowing.	LPAR	1992	DBLP DOI BibTeX RDF
2	Luís Moniz Pereira, Luís Caires, José Júlio Alferes	SLWV - A Theorem Prover for Logic Programming.	ELP	1992	DBLP DOI BibTeX RDF
2	Joakim von Wright, Thomas Långbacka	Using a Theorem Prover for Reasoning about Concurrent Algorithms.	CAV	1992	DBLP DOI BibTeX RDF
2	Robert S. Boyer, Yuan Yu	Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor.	CADE	1992	DBLP DOI BibTeX RDF	Nqthm, Boyer-Moore Theorem Prover, Gnu, Ada, C, Automated reasoning, object code, formal program verification