Search results for "theorem-prover"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
23	Alessandro Avellone, Marco Benini, Ugo Moscato	How to Avoid the Formal Verification of a Theorem Prover.	Log. J. IGPL	2001	DBLP DOI BibTeX RDF
23	Yves Bertot	Formalizing a JVML Verifier for Initialization in a Theorem Prover.	CAV	2001	DBLP DOI BibTeX RDF
23	Iara Moema Oberg Vilela, Priscila Machado Vieira Lima	Conjecturing the Cognitive Plausibility of an ANN Theorem-Prover.	IWANN (1)	2001	DBLP DOI BibTeX RDF
23	Vanderlei Moraes Rodrigues, Dominique Borrione, Philippe Georgelin	Using the ACL2 Theorem Prover to Reason about VHDL Components.	RITA	2000	DBLP BibTeX RDF
23	Hiroshi Sakai, Akimichi Okuma	On a Theorem Prover for Variational Logic Programs with Functors Setu and Sets.	Int. J. Uncertain. Fuzziness Knowl. Based Syst.	2000	DBLP DOI BibTeX RDF
23	Lila Rao, Han Reichgelt	STIRDAT: A system tightly integrating relational databases and a theorem prover.	Data Knowl. Eng.	2000	DBLP DOI BibTeX RDF
23	Dirk Fuchs	Cooperation in heterogeneous theorem prover networks.		2000	RDF
23	Ulrich Kühler	A tactic-based inductive theorem prover for data types with partial operations.		2000	RDF
23	Joachim Draeger	Redundancy-Free Lemmatization in the Automated Model-Elimination Theorem Prover AI-SETHEO.	TABLEAUX	2000	DBLP DOI BibTeX RDF
23	Gernot Stenz, Andreas Wolf 0005	E-SETHEO: An Automated3 Theorem Prover.	TABLEAUX	2000	DBLP DOI BibTeX RDF
23	Ivan I. Garibay	Generating Text with a Theorem Prover.	ANLP	2000	DBLP BibTeX RDF
23	Allen Van Gelder, Fumiaki Okushi	A propositional theorem prover to solve planning and other problems.	Ann. Math. Artif. Intell.	1999	DBLP DOI BibTeX RDF
23	Jussi Rintanen	Constructing Conditional Plans by a Theorem-Prover.	J. Artif. Intell. Res.	1999	DBLP DOI BibTeX RDF
23	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
23	José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo, Francisco-Jesús Martín-Mateos	Mechanical verification of a rule-based unification algorithm in the Boyer-Moore theorem prover.	APPIA-GULP-PRODE	1999	DBLP BibTeX RDF
23	Jean-Michel Richer, Jean-Jacques Chabrier	Sacre: a Constraint Satisfaction Problem Based Theorem Prover.	AAAI/IAAI	1999	DBLP BibTeX RDF
23	Andrei Voronkov	KK: a theorem prover for K.	CADE	1999	DBLP DOI BibTeX RDF
23	Dieter Hutter, Alan Bundy	The Design of the CADE-16 Inductive Theorem Prover Contest.	CADE	1999	DBLP DOI BibTeX RDF
23	Ulrich Endriss	A Time Efficient KE Based Theorem Prover.	TABLEAUX	1999	DBLP DOI BibTeX RDF
23	Alvaro Kilkerry Neto, Gerson Zaverucha, Luís Alfredo Vidal de Carvalho	An implementation of a theorem prover in symmetric neural networks.	IJCNN	1999	DBLP DOI BibTeX RDF
23	Robert F. Stärk	The Theoretical Foundations of LPTP (A Logic Program Theorem Prover).	J. Log. Program.	1998	DBLP DOI BibTeX RDF
23	Tristan Cazenave	Synthesis of an Efficient Tactical Theorem Prover for the Game of Go.	ACM Comput. Surv.	1998	DBLP DOI BibTeX RDF
23	Peter Jakobi, Andreas Wolf	DBFW: A Simple DataBase FrameWork for the Evaluation and Maintenance of Automated Theorem Prover Data.	CSMR	1998	DBLP DOI BibTeX RDF
23	Christoph Benzmüller, Michael Kohlhase	System Description: LEO - A Higher-Order Theorem Prover.	CADE	1998	DBLP DOI BibTeX RDF
23	Matt Kaufmann, J Strother Moore	An Industrial Strength Theorem Prover for a Logic Based on Common Lisp.	IEEE Trans. Software Eng.	1997	DBLP DOI BibTeX RDF	total functions, microcode verification, floating point division, Formal verification, digital signal processing, type checking, computational logic, automatic theorem proving, partial functions
23	M. Paramasivam, David A. Plaisted	RRTP - A Replacement Rule Theorem Prover.	J. Autom. Reason.	1997	DBLP DOI BibTeX RDF
23	Christian B. Suttner	SPTHEO - A Parallel Theorem Prover.	J. Autom. Reason.	1997	DBLP DOI BibTeX RDF
23	Heng Chu, David A. Plaisted	CLIN-S - A Semantically Guided First-Order Theorem Prover.	J. Autom. Reason.	1997	DBLP DOI BibTeX RDF
23	Thomas Kolbe, Sabine Glesner	Many-Sorted Logic in a Learning Theorem Prover.	KI	1997	DBLP DOI BibTeX RDF
23	Thomas R. Ioerger	Integrating a Spatial Reasoner with a Resolution Theorem-Prover.	AAAI/IAAI	1997	DBLP BibTeX RDF
23	Ryuzo Hasegawa, Hiroshi Fujita 0002, Miyuki Koshimura	MGTP: A Model Generation Theorem Prover - Its Advanced Features and Applications.	TABLEAUX	1997	DBLP DOI BibTeX RDF
23	Jens Otten	ileanTAP: An Intuitionistic Theorem Prover.	TABLEAUX	1997	DBLP DOI BibTeX RDF
23	Robert Sandner, Olaf Müller	Theorem Prover Support for the Refinement of Stream Processing Functions.	TACAS	1997	DBLP DOI BibTeX RDF
23	Christian B. Suttner	SPTHEO - A PVM-Based Parallel Theorem Prover.	PVM	1996	DBLP DOI BibTeX RDF
23	Robert Geisler, Marcus Klar, Felix Cornelius	InterACT: An Interactive Theorem Prover for Algebraic Specifications.	AMAST	1996	DBLP DOI BibTeX RDF
23	Chandrabose Aravindan	DisLoP: A Disjunctive Logic Programming System Based on PROTEIN Theorem Prover.	KI	1996	DBLP DOI BibTeX RDF
23	Roderick Moten	Nuprl as a concurrent interactive theorem prover.	African Americans in Mathematics	1996	DBLP DOI BibTeX RDF
23	Dongming Wang 0001	GEOTHER: A Geometry Theorem Prover.	CADE	1996	DBLP DOI BibTeX RDF
23	Bernhard Beckert, Reiner Hähnle, Peter Oel, Martin Sulzmann	The Tableau-based Theorem Prover 3TAP Version 4.0.	CADE	1996	DBLP DOI BibTeX RDF
23	Shie-Jue Lee, David A. Plaisted	Controlling the Consumption of Storage with Sliding Priority Search in a Hyper-Linking Based Theorem Prover.	Comput. Artif. Intell.	1995	DBLP BibTeX RDF
23	Jérôme Mengin	A Theorem Prover for Default Logic Based on Prioritized Conflict Resolution and an Extended Resolution Principle.	ECSQARU	1995	DBLP DOI BibTeX RDF
23	Pascal Nicolas, Béatrice Duval	A Theorem Prover for Lukaszewicz' Open Default Theory.	ECSQARU	1995	DBLP DOI BibTeX RDF
23	Anna Formica, Michele Missikoff, Roberto Terenzi	A Theorem Prover for Checking Satisfiability of Object-Oriented Database Schemas.	ICLP	1995	DBLP BibTeX RDF
23	Laurence Pierre	Describing and verifying synchronous circuits with the Boyer-Moore theorem prover.	CHARME	1995	DBLP DOI BibTeX RDF
23	Slim Abdennadher, François Bry, Norbert Eisinger, Tim Geisler	The theorem prover SATCHMO : strategies, heuristics and applications.	JFPLC	1995	DBLP BibTeX RDF
23	Johann Schumann	Using the Theorem Prover SETHEO for Verifying the Development of a Communication Protocol in FOCUS: A Case Study.	TABLEAUX	1995	DBLP DOI BibTeX RDF
23	Pascal Nicolas, Béatrice Duval	Lukaszewicz' Default Logic: A Theorem Prover Based on SLD-Resolution for Open Default Theory.	WOCFAI	1995	DBLP BibTeX RDF
23	Shie-Jue Lee, David A. Plaisted	Problem Solving by Searching for Models with a Theorem Prover.	Artif. Intell.	1994	DBLP DOI BibTeX RDF
23	Shie-Jue Lee, Chih-Hung Wu	Improving the Efficiency of a Hyperlinking-Based Theorem Prover by Incremental Evaluation with Network Structures.	J. Autom. Reason.	1994	DBLP DOI BibTeX RDF
23	Lawrence C. Paulson	Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow)		1994	DOI RDF
23	Alberto Artosi, Paola Cattabriga, Guido Governatori	KED: A Deontic Theorem Prover.	ICLP Workshop: Legal Application of Logic Programming	1994	DBLP BibTeX RDF
23	Joakim von Wright	Program Refinement by Theorem Prover.	Refine	1994	DBLP DOI BibTeX RDF
23	Alessandro Armando, Enrico Giunchiglia	Embedding Complex Decision Procedures Inside an Interactive Theorem Prover.	Ann. Math. Artif. Intell.	1993	DBLP DOI BibTeX RDF
23	Lawrence C. Paulson	The Foundation of a Generic Theorem Prover	CoRR	1993	DBLP BibTeX RDF
23	Lawrence C. Paulson	Designing a Theorem Prover	CoRR	1993	DBLP BibTeX RDF
23	Javier Leach, Susana Nieva	Foundations of a theorem prover for functional and mathematical uses.	J. Appl. Non Class. Logics	1993	DBLP DOI BibTeX RDF
23	J. E. Heaton, Pavel Kocura	Presenting a Pierce Logic Based Inference Engine and Theorem Prover for Conceptual Graphs.	ICCS	1993	DBLP DOI BibTeX RDF
23	Shie-Jue Lee, Chih-Hung Wu	Improving Efficiency of a Theorem Prover by Eliminating Redundant Unifications Using Network Structures.	ICCI	1993	DBLP BibTeX RDF
23	John K. Slaney	SCOTT: A Model-Guided Theorem Prover.	IJCAI	1993	DBLP BibTeX RDF
23	Richard J. Boulton	Efficiency in a fully-expansive theorem prover.		1993	RDF
23	Reiner Hähnle, Bernhard Beckert, Stefan Gerberding, Werner Kernig	The Many-Valued Theorem Prover 3TAP.	IWBS Report	1992	RDF
23	Mark E. Stickel	A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog.	Theor. Comput. Sci.	1992	DBLP DOI BibTeX RDF
23	James D. Baker, Shariar Zand-Biglari	An Integral Theorem Prover And The Role Of Proof Planning.	J. Autom. Reason.	1992	DBLP DOI BibTeX RDF
23	Reinhold Letz, Johann Schumann, Stefan Bayerl, Wolfgang Bibel	SETHEO: A High-Performance Theorem Prover.	J. Autom. Reason.	1992	DBLP DOI BibTeX RDF
23	Soumitra Bose, Edmund M. Clarke, David E. Long, Spiro Michaylov	PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses.	J. Autom. Reason.	1992	DBLP DOI BibTeX RDF
23	Matt Kaufmann	An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification.	J. Autom. Reason.	1992	DBLP DOI BibTeX RDF
23	Dan Sahlin, Torkel Franzén, Seif Haridi	An Intuitionistic Predicate Logic Theorem Prover.	J. Log. Comput.	1992	DBLP DOI BibTeX RDF
23	Ursula Martin, Michael Lai	Some Experiments with a Completion Theorem Prover.	J. Symb. Comput.	1992	DBLP DOI BibTeX RDF
23	Javier Leach, Susana Nieva	MIZ-PR: A Theorem Prover for Polymorphic and Recursive Functions.	LPAR	1992	DBLP DOI BibTeX RDF
23	Adel Bouhoula, Emmanuel Kounalis, Michaël Rusinowitch	SPIKE, an Automatic Theorem Prover.	LPAR	1992	DBLP DOI BibTeX RDF
23	Monica Nesi	Formalizing a Modal Logic for CSS in the HOL Theorem Prover.	TPHOLs	1992	DBLP BibTeX RDF
23	Manfred R. Jobmann, Johann Schumann	Modelling and Performances Analysis of a Parallel Theorem Prover.	SIGMETRICS	1992	DBLP DOI BibTeX RDF
23	Dave Barker-Plummer, Alex Rothenberg	The GAZER Theorem Prover.	CADE	1992	DBLP DOI BibTeX RDF
23	Bernhard Beckert, Stefan Gerberding, Reiner Hähnle, Werner Kernig	The Tableau-Based Theorem Prover 3TAP for Multi-Valued Logics.	CADE	1992	DBLP DOI BibTeX RDF
23	Ewing L. Lusk, William McCune, John K. Slaney	ROO: A Parallel Theorem Prover.	CADE	1992	DBLP DOI BibTeX RDF
23	Shang-Ching Chou	A Geometry Theorem Prover for Macintoshes.	CADE	1992	DBLP DOI BibTeX RDF
23	Edmund M. Clarke, Xudong Zhao 0005	Analytica - A Theorem Prover in Mathematica.	CADE	1992	DBLP DOI BibTeX RDF
23	Johann Schumann	KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract).	CADE	1992	DBLP DOI BibTeX RDF
23	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
23	Holger Busch	Transformational Design in a Theorem Prover.	TPCD	1992	DBLP BibTeX RDF
23	Philippe Lamarre	A Tableau Like Theorem Prover for Conditional Logics (Extended Abstract).	TABLEAUX	1992	DBLP BibTeX RDF
23	Wilfried Neitz	A Connection Method based Theorem Prover with Selective Backtracking (Extended Abstract).	TABLEAUX	1992	DBLP BibTeX RDF
23	Charles G. Morgan	An Automated Theorem Prover for Relational Logic (Abstract).	TABLEAUX	1992	DBLP BibTeX RDF
23	Philippe Lamarre	A Promenade from Monotonicity to Non-Monotonicity Following a Theorem Prover.	KR	1992	DBLP BibTeX RDF
23	Manfred R. Jobmann, Johann Schumann	Modelling and performance analysis of a parallel theorem prover	Forschungsberichte, TU Munich	1991	RDF
23	Wen-Tsuen Chen, Tzren-Ru Chou, Kuen-Rong Hsieh, Huai-Jen Liu	Design of a Parallel Theorem Prover for First Order Logic.	J. Inf. Sci. Eng.	1991	DBLP BibTeX RDF
23	Christine Lafontaine, Yves Ledru, Pierre-Yves Schobbens	An Experiment in Formal Software Development: Using the B Theorem Prover on a VDM Case Study.	Commun. ACM	1991	DBLP DOI BibTeX RDF
23	Laurent Catach	TABLEAUX: A General Theorem Prover for Modal Logics.	J. Autom. Reason.	1991	DBLP DOI BibTeX RDF
23	Manfred R. Jobmann, Johann Schumann	Modelling and performance Analysis of a Parallel Theorem Prover.	MMB	1991	DBLP DOI BibTeX RDF
23	Hiroshi Fujita 0002, Ryuzo Hasegawa	A Model Generation Theorem Prover in KL1 Using a Ramified -Stack Algorithm.	ICLP	1991	DBLP BibTeX RDF
23	Wen-Tsuen Chen, Tzren-Ru Chou, Kuen-Rong Hsieh, Huai-Jen Liu	Design of a parallel theorem prover for first order logic.	COMPSAC	1991	DBLP DOI BibTeX RDF
23	Christian B. Suttner, Wolfgang Ertel	Using connectionist networks for guiding the search of a theorem prover	Forschungsberichte, TU Munich	1990	RDF
23	Johann Schumann, Reinhold Letz	PARTHEO: a high performance parallel theorem prover	Forschungsberichte, TU Munich	1990	RDF
23	Albert John Camilleri	Reasoning in CSP via the HOL theorem prover.	Jerusalem Conference on Information Technology	1990	DBLP DOI BibTeX RDF
23	Christian B. Suttner	A Parallel Theorem Prover with Heuristic Work Distribution.	Dagstuhl Seminar on Parallelization in Inference Systems	1990	DBLP DOI BibTeX RDF
23	Christian B. Suttner	Representing Heuristic-Relevant Information for an Automated Theorem Prover.	IMYCS	1990	DBLP DOI BibTeX RDF
23	Neil V. Murray, Erik Rosenthal	DISSOLVER: A Dissolution-based Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF
23	Ralph Butler, Ian T. Foster, Anita Jindal, Ross A. Overbeek	A High-Performance Parallel Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF
23	Mark E. Stickel	A Prolog Technology Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF
23	Geoff Sutcliffe	A General Clause Theorem Prover.	CADE	1990	DBLP DOI BibTeX RDF