Search results for "theorem-prover"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
74	Dipankar Sarkar 0001, 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
72	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
69	George C. Necula, Peter Lee 0001	Proof Generation in the Touchstone Theorem Prover.	CADE	2000	DBLP DOI BibTeX RDF
67	Stefan Gerberding	DT - An Automated Theorem Prover for Multiple-Valued First-Order Predicate Logics.	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
66	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
65	Yoshinao Isobe, Markus Roggenbach	A Generic Theorem Prover of CSP Refinement.	TACAS	2005	DBLP DOI BibTeX RDF
64	Anand Chavan, Shiu-Kai Chin, Shahid Ikram, Jang Dae Kim, Juin-Yeu Zu	Extending VLSI design with higher-order logic.	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
61	Robert S. Boyer, J Strother Moore	A Theorem Prover for a Computational Logic.	CADE	1990	DBLP DOI BibTeX RDF
59	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
58	Maarten de Mol, Marko C. J. D. van Eekelen	A Proof Tool Dedicated to Clean - The First Prototype.	AGTIVE	1999	DBLP DOI BibTeX RDF
56	Kenneth Roe	The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover.	CAV	2006	DBLP DOI BibTeX RDF
55	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
55	Jun Sawada, Erik Reeber	ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool.	FMCAD	2006	DBLP DOI BibTeX RDF
55	Blayne E. Mayfield, Timothy B. Baird	STP: A Simple Theorem Prover for IBM-PC Compatible Computers.	SIGSMALL/PC Symposium	1990	DBLP DOI BibTeX RDF	IBM PC, Turbo Pascal
55	Jieh Hsiang, Mandayam K. Srivas	PROLOG-Based Inductive Theorem Proving.	FSTTCS	1985	DBLP DOI BibTeX RDF
54	Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt	System Description: card TAP: The First Theorem Prover on a Smart Card.	CADE	1998	DBLP DOI BibTeX RDF
52	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
52	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
52	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
51	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
51	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
49	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
49	Ian Horrocks 0001, Andrei Voronkov	Reasoning Support for Expressive Ontology Languages Using a Theorem Prover.	FoIKS	2006	DBLP DOI BibTeX RDF
48	Marcel Oliveira, Ana Cavalcanti 0001, Jim Woodcock 0001	Unifying Theories in ProofPower-Z.	UTP	2006	DBLP DOI BibTeX RDF	Unifying Theories of Programming, theorem prover
48	Mizuhito Ogawa, Eiichi Horita, Satoshi Ono	Proving Properties of Incremental Merkle Trees.	CADE	2005	DBLP DOI BibTeX RDF	temporal authentication, theorem prover, Merkle tree
48	Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita 0002	MGTP: A Parallel Theorem Prover Based on Lazy Model Generation.	CADE	1992	DBLP DOI BibTeX RDF
48	Mark Tarver	An Examination of the Prolog Technology Theorem-Prover.	CADE	1990	DBLP DOI BibTeX RDF	PTTP, metalevel reasoning, Prolog Normal Form, refinement
47	Virginie Thion, Serenella Cerrito, Marta Cialdea Mayer	A General Theorem Prover for Quantified Modal Logics.	TABLEAUX	2002	DBLP DOI BibTeX RDF
47	Tanel Tammet	A Resolution Theorem Prover for Intuitonistic Logic.	CADE	1996	DBLP DOI BibTeX RDF
47	Gernot Stenz, Andreas Wolf 0005	Scheduling Methods for Parallel Automated Theorem Proving.	AI	2000	DBLP DOI BibTeX RDF
45	Mihir Parang Mehta	Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32.	ACL2	2018	DBLP DOI BibTeX RDF
45	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
44	Johann Schumann, Bernd Fischer 0002	NORA/HAMMR: Making Deduction-Based Software Component Retrieval Practical.	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
44	Dru McCandless, Leo Obrst, Shayn Hawthorne	Dynamic Web Service Assembly Using OWL and a Theorem Prover.	ICSC	2009	DBLP DOI BibTeX RDF
44	Aaron Richard Coble	Formalized Information-Theoretic Proofs of Privacy Using the HOL4 Theorem-Prover.	Privacy Enhancing Technologies	2008	DBLP DOI BibTeX RDF
44	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
44	Tadashi Takahashi, Hidetsune Kobayashi	The Effect of the Theorem Prover in Cognitive Science.	International Conference on Computational Science (1)	2006	DBLP DOI BibTeX RDF
44	Nicola Olivetti, Gian Luca Pozzato	CondLean: A Theorem Prover for Conditional Logics.	TABLEAUX	2003	DBLP DOI BibTeX RDF
44	Jens Happe	The MODPROF Theorem Prover.	IJCAR	2001	DBLP DOI BibTeX RDF
44	David Spelt, Susan Even	A Theorem Prover-Based Analysis Tool for Object-Oriented Databases.	TACAS	1999	DBLP DOI BibTeX RDF
44	Aline Deruyver	EMMY: A Refutational Theorem Prover for First-Order Logic with Equation.	RTA	1991	DBLP DOI BibTeX RDF
44	Johann Schumann, Reinhold Letz	PARTHEO: A High-Performance Parallel Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF	Warren Abstract Machine, message passing, Theorem proving, first-order logic, transputers, or-parallelism, model elimination, connection method
44	Heikki Tuominen	Proving Properties of Elementary Net Systems with a Special-Purpose Theorem Prover.	Automatic Verification Methods for Finite State Systems	1989	DBLP DOI BibTeX RDF
44	Mark E. Stickel	A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler.	CADE	1986	DBLP DOI BibTeX RDF
44	Paul Y. Gloess	An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions.	CADE	1980	DBLP DOI BibTeX RDF
43	John Matthews, J Strother Moore, Sandip Ray, Daron Vroon 0001	Verification Condition Generation Via Theorem Proving.	LPAR	2006	DBLP DOI BibTeX RDF
43	Michael Barnett 0001, K. Rustan M. Leino	Weakest-precondition of unstructured programs.	PASTE	2005	DBLP DOI BibTeX RDF
43	Deepak Kapur, Mahadevan Subramaniam	Using an induction prover for verifying arithmetic circuits.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	Induction, Automated reasoning, Decision procedures, Rewriting, Arithmetic circuits, Hardware verification
43	Dennis de Champeaux	Subproblem finder and instance checker, two cooperating modules for theorem provers.	J. ACM	1986	DBLP DOI BibTeX RDF
41	Osman Hasan, Sofiène Tahar	Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Real-time systems, Communication protocols, Higher-order-logic, Probability theory, HOL theorem prover
41	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
41	Wendy MacCaull	Finite Algebraic Models for Residuated Logic.	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
41	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
41	Xia Wu, Jigui Sun, Kun Hou	An Extension Rule Based First-Order Theorem Prover.	KSEM	2006	DBLP DOI BibTeX RDF
41	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
41	Koji Iwanuma	Lemma Matching for a PTTP-based Top-down Theorem Prover.	CADE	1997	DBLP DOI BibTeX RDF
41	Hans Jürgen Ohlbach, Graham Wrightson	Solving a Problem in Relevance Logic with an Automated Theorem Prover.	CADE	1984	DBLP DOI BibTeX RDF
40	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
40	Richard Bonichon, David Delahaye, Damien Doligez	Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs.	LPAR	2007	DBLP DOI BibTeX RDF
40	Kaustuv Chaudhuri, Frank Pfenning	A Focusing Inverse Method Theorem Prover for First-Order Linear Logic.	CADE	2005	DBLP DOI BibTeX RDF
40	Kenneth L. McMillan	An Interpolating Theorem Prover.	TACAS	2004	DBLP DOI BibTeX RDF
40	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
40	Yves Ledru	Identifying Pre-Conditions with the Z/EVES Theorem Prover.	ASE	1998	DBLP DOI BibTeX RDF
40	Maria Paola Bonacina	The Clause-Diffusion Theorem Prover Peers-mcd (System Description).	CADE	1997	DBLP DOI BibTeX RDF
40	Scott Hazelhurst, Carl-Johan H. Seger	A simple theorem prover based on symbolic trajectory evaluation and BDD's.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	1995	DBLP DOI BibTeX RDF
39	Jens Otten	leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions).	IJCAR	2008	DBLP DOI BibTeX RDF
38	Adolfo Gustavo Serra Seca Neto, Marcelo Finger	Effective Prover for Minimal Inconsistency Logic.	IFIP AI	2006	DBLP DOI BibTeX RDF
38	Mario Carneiro	Metamath Zero: Designing a Theorem Prover Prover.	CICM	2020	DBLP DOI BibTeX RDF
38	Shuling Wang, Naijun Zhan, Liang Zou	An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems.	ICFEM	2015	DBLP DOI BibTeX RDF
38	Aleksandar Krapez, Miodrag Kapetanovic, Zoran Ognjanovic, Tatjana Petrovic	Prover 91 - A Parallel Theorem Prover (Extended Abstract).	TABLEAUX	1992	DBLP BibTeX RDF
38	Steven Greenbaum, David A. Plaisted	The Illinois Prover: A General Purpose Resolution Theorem Prover.	CADE	1986	DBLP DOI BibTeX RDF
38	Shang-Ching Chou	GEO-Prover - A Geometry Theorem Prover Developed at UT.	CADE	1986	DBLP DOI BibTeX RDF
38	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
38	Osman Hasan, Sofiène Tahar	Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Coupon collector’s problem, Probabilistic analysis, Higher-order-logic, Probability theory, Statistical properties, HOL theorem prover
38	Julien Narboux	A Graphical User Interface for Formal Proofs in Geometry.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Interface, Geometry, Automated theorem proving, Theorem prover, Proof assistant, Coq, Dynamic geometry
38	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
38	Keith Vanderveen, C. V. Ramamoorthy	Partial instantiation theorem proving for distributed resource location.	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
38	Dieter Fensel, Arno Schönegge	Using KIV to Specify and Verify Architectures of Knowledge-Based Systems.	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
38	Savi Maharaj, Juan Bicarregui	On the Verification of VDM Specification and Refinement with PVS.	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
38	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
38	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
38	David Cyrluk, Mandayam K. Srivas	Theorem proving: not an esoteric diversion, but the unifying framework for industrial verification.	ICCD	1995	DBLP DOI BibTeX RDF	industrial hardware verification, industrial verification, formal verification, logic testing, theorem proving, theorem prover, hardware verification
38	Ramayya Kumar, Thomas Kropf, Klaus Schneider 0001	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
38	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
38	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
38	Gerald M. Karam, Raymond J. A. Buhr	Temporal Logic-Based Deadlock Analysis For Ada.	IEEE Trans. Software Eng.	1991	DBLP DOI BibTeX RDF	temporal logic-based specification language, deadlock analyzer, Timebench, concurrent system-design environment, COL, linear-time temporal logic, formal basis, axiomatic reasoning, deadlock analysis tool, reasoning power, Ada designs, systemwide deadlock-free, deadlock algorithm, finite systems, worst-case computational complexity, gas station, layered communications system, computational complexity, Ada, logic programming, temporal logic, Prolog, specification language, specification languages, inference mechanisms, system recovery, theorem prover, readers, dining philosophers, writers
38	William R. Bevier, Jørgen F. Søgaard-Andersen	Mechanically Checked Proofs of Kernel Specification.	CAV	1991	DBLP DOI BibTeX RDF	mechanical proof checking, Boyer-Moore Theorem Prover, Kernel, labeled transition systems, safety properties, stepwise development
38	Albert John Camilleri	Mechanizing CSP Trace Theory in Higher Order Logic.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	mechanising CSP trace theory, general-purpose theorem prover, formal specification, theorem proving, formal logic, higher order logic, communicating sequential processes
38	Dipankar Sarkar 0001, S. C. De Sarkar	Some Inference Rules for Integer Arithmetic for Verification of Flowchart Programs on Integers.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	flowchart programs, first-order rules, algebraic expressions, proof construction process, human thought process, user provided axioms, verification, theorem proving, program verification, inference mechanisms, inference rules, theorem prover, integer arithmetic
38	William R. Bevier	Kit: A Study in Operating System Verification.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	multitasking operating system kernel, machine language, uniprocessor von Neumann computer, conceptually distributed communicating processes, asynchronous devices, security-related results, supervisor mode, Boyer-Moore logic, Boyer-Moore theorem prover, verification, interface, message passing, theorem proving, program verification, operating systems (computers), multiprogramming, correctness proof, process scheduling, error handling, Kit
37	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
37	Dale Vaillancourt, Rex L. Page, Matthias Felleisen	ACL2 in DrScheme.	ACL2	2006	DBLP DOI BibTeX RDF	DrScheme, TeachScheme!, formal methods, pedagogy, ACL2
37	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
37	Hasan Amjad	Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover.	TPHOLs	2003	DBLP DOI BibTeX RDF
37	Gernot Stenz, Andreas Wolf 0005	E-SETHEO: Design, Configuration and Use of a Parallel Automated Theorem Prover.	Australian Joint Conference on Artificial Intelligence	1999	DBLP DOI BibTeX RDF
37	Deepak Kapur, Mahadevan Subramaniam	Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover.	ASIAN	1998	DBLP DOI BibTeX RDF
37	Sten Agerholm, Jacob Frost	An Isabelle-Based Theorem Prover for VDM-SL.	TPHOLs	1997	DBLP DOI BibTeX RDF
37	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
37	Mark E. Stickel	A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog.	DISCO	1990	DBLP DOI BibTeX RDF
37	Weiqiang Kong, Takahiro Seino, Kokichi Futatsugi, Kazuhiro Ogata 0001	A Lightweight Integration of Theorem Proving and Model Checking for System Verification.	APSEC	2005	DBLP DOI BibTeX RDF