|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 1960 occurrences of 846 keywords
|
|
|
Results
Found 3383 publication records. Showing 3383 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
84 | Quan Liu, Yang Gao 0001, Zhiming Cui, WangShu Yao, ZhongWen Chen |
An Tableau Automated Theorem Proving Method Using Logical Reinforcement Learning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISICA ![In: Advances in Computation and Intelligence, Second International Symposium, ISICA 2007, Wuhan, China, September 21-23, 2007, Proceedings, pp. 262-270, 2007, Springer, 978-3-540-74580-8. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
logical reinforcement learning, tableau automated theorem proving, LOMDP |
75 | Sandip Ray, Rob Sumners |
Combining Theorem Proving with Model Checking through Predicate Abstraction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Des. Test Comput. ![In: IEEE Des. Test Comput. 24(2), pp. 132-139, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
model checking, formal verification, theorem proving, predicate abstraction, ACL2 |
75 | Sun Yong-qiang, Lu Ru-zhan, Bi Hua |
Program synthesis based on Boyer-Moore theorem proving techniques. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Conference on Computer Science ![In: Proceedings of the 13th ACM Annual Conference on Computer Science, New Orleans, Louisiana, USA, 1985, pp. 348-355, 1985, ACM, 0-89791-150-4. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
Boyer-Moore technique, program sysnthesis, theorem proving, resolution |
71 | Youngsik Kim, Parija Sule, Nazanin Mansouri |
Exploiting PSL standard assertions in a theorem-proving-based verification environment. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Great Lakes Symposium on VLSI ![In: Proceedings of the 15th ACM Great Lakes Symposium on VLSI 2005, Chicago, Illinois, USA, April 17-19, 2005, pp. 400-403, 2005, ACM, 1-59593-057-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
assertion-based design, modeling, verification, theorem-proving, formal semantics, PSL |
70 | Maria Paola Bonacina, Jieh Hsiang |
On Fairness of Completion-Based Theorem Proving Strategies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, pp. 348-360, 1991, Springer, 3-540-53904-2. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
67 | Sreeranga P. Rajan, Jeffrey J. Joyce, Carl-Johan H. Seger |
From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HUG ![In: Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings, pp. 489-500, 1993, Springer, 3-540-57826-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
66 | Wing-Kwong Wong, Bo-Yu Chan, Sheng-Kai Yin |
A Dynamic Geometry Environment for Learning Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALT ![In: Proceedings of the 5th IEEE International Conference on Advanced Learning Technologies, ICALT 2005, Kaohsiung, Taiwan, July 5-8, 2005, pp. 15-17, 2005, IEEE Computer Society, 0-7695-2338-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
learning geometry, geometry education, theorem proving, Dynamic geometry |
66 | Hongbo Li 0012 |
Algebraic Representation, Elimination and Expansion in Automated Geometric Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry, 4th International Workshop, ADG 2002, Hagenberg Castle, Austria, September 4-6, 2002, Revised Papers, pp. 106-123, 2002, Springer, 3-540-20927-1. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Cayley algebra, bracket algebra, affine geometry, automated theorem proving, projective geometry, conics |
66 | Miroslav Popovic, Vladimir Kovacevic, Ivan Velikic |
A Formal Software Verification Concept Based on Automated Theorem Proving and Reverse Engineering. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ECBS ![In: 9th IEEE International Conference on Engineering of Computer-Based Systems (ECBS 2002), 8-11 April 2002, Lund, Sweden, pp. 59-66, 2002, IEEE Computer Society, 0-7695-1549-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
formal software verification, fault-tolerant and robust software, mission-critical embedded software, reverse engineering, automated theorem proving, predicate calculus |
66 | Fausto Giunchiglia, Paolo Traverso |
Theorem proving in technology transfer: the user's point of view. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 3(1), pp. 1-12, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Formal methods, Mechanized theorem proving |
65 | Jieh Hsiang, Mandayam K. Srivas |
PROLOG-Based Inductive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSTTCS ![In: Foundations of Software Technology and Theoretical Computer Science, Fifth Conference, New Delhi, India, December 16-18, 1985, Proceedings, pp. 129-149, 1985, Springer, 3-540-16042-6. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
|
64 | Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger |
Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, pp. 323-340, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
62 | Larry Wos |
Solving Open Questions with an Automated Theorem-Proving Program. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 6th Conference on Automated Deduction, New York, USA, June 7-9, 1982, Proceedings, pp. 1-31, 1982, Springer, 3-540-11558-7. The full citation details ...](Pics/full.jpeg) |
1982 |
DBLP DOI BibTeX RDF |
|
62 | Weiqiang Kong, Takahiro Seino, Kokichi Futatsugi, Kazuhiro Ogata 0001 |
A Lightweight Integration of Theorem Proving and Model Checking for System Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APSEC ![In: 12th Asia-Pacific Software Engineering Conference (APSEC 2005), 15-17 December 2005, Taipei, Taiwan, pp. 59-66, 2005, IEEE Computer Society, 0-7695-2465-6. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
61 | Chih-Hung Wu, Shie-Jue Lee |
On parallelism of hyper-linking theorem proving: a preliminary report. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICPADS ![In: 1996 International Conference on Parallel and Distributed Systems (ICPADS '96), June 3-6, 1996, Tokyo, Japan, Proceedings, pp. 494-499, 1996, IEEE Computer Society, 0-8186-7267-6. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
hyper-linking theorem proving, hyper-linking proof procedure, phase-level, clause-level, literal-level, search level parallelism, parallel strategies, parallel algorithms, parallelism, artificial intelligence, parallel architectures, theorem proving |
61 | Ming-Yi Fang, Wen-Tsuen Chen |
Vectorization of a Generalized Procedure for Theorem Proving in Propositional Logic on Vector Computers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Knowl. Data Eng. ![In: IEEE Trans. Knowl. Data Eng. 4(5), pp. 475-486, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
artificial intelligence, theorem proving, theorem proving, formal logic, propositional logic, vector processor systems, vectorisation, vector computers, deduction rules |
60 | Yuyan Chao, Lifeng He, Tsuyoshi Nakamura, Zhenghao Shi, Kenji Suzuki 0001, Hidenori Itoh |
An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Comput. Sci. Technol. ![In: J. Comput. Sci. Technol. 22(4), pp. 541-553, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Herbrand’s theorem, Herbrand universe, model generation theorem proving, SATCHMO, really non-propositinal |
59 | Naren Narasimhan, Ranga Vemuri |
On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, pp. 367-386, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
58 | David R. Lester |
Real Number Calculations and Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 215-229, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Computable Reals, Exact Arithmetic, Theorem Proving, PVS, Higher-order Logic |
57 | Yingying Jiang 0001, Feng Tian 0001, Hongan Wang, Xiaolong Zhang 0001, XuGang Wang, Guozhong Dai |
Intelligent understanding of handwritten geometry theorem proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IUI ![In: Proceedings of the 15th International Conference on Intelligent User Interfaces, IUI 2010, Hong Kong, China, February 7-10, 2010, pp. 119-128, 2010, ACM, 978-1-60558-515-4. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
geometry theorem proving, hand-drawn figures, hand-written proof scripts, structure based manipulation, recognition |
57 | Hai Lin 0008, Jigui Sun, Yimin Zhang 0005 |
Theorem Proving Based on the Extension Rule. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 31(1), pp. 11-21, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
extension rule, inclusion-exclusion principle, complementary factor, theorem proving |
57 | Gilles Dowek, Thérèse Hardin, Claude Kirchner |
Theorem Proving Modulo. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 31(1), pp. 33-72, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
sequent calculus modulo, resolution, rewriting, automated theorem proving, higher-order logic, cut elimination, narrowing, Skolemization, deduction modulo |
57 | Simon J. Gay |
A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 217-232, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
semantics, Types, pi calculus, automatic theorem proving |
56 | David A. Plaisted |
Special Cases and Substitutes for Rigid E-Unification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Appl. Algebra Eng. Commun. Comput. ![In: Appl. Algebra Eng. Commun. Comput. 10(2), pp. 97-152, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Rigid E -unification, Theorem proving, First-order logic, Decidability, Unification, Equality, Horn clauses, Tableaux |
54 | Christoph Benzmüller, Andreas Meier 0002, Volker Sorge |
Bridging Theorem Proving and Mathematical Knowledge Retrieval. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Mechanizing Mathematical Reasoning ![In: Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday, pp. 277-296, 2005, Springer, 3-540-25051-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
54 | Helko Lehmann, Michael Leuschel |
Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LOPSTR ![In: Logic Based Program Synthesis and Transformation, 13th International Symposium LOPSTR 2003, Uppsala, Sweden, August 25-27, 2003, Revised Selected Papers, pp. 1-19, 2003, Springer, 3-540-22174-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
52 | Panagiotis Manolios, Daron Vroon 0001 |
Integrating static analysis and general-purpose theorem proving for termination analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICSE ![In: 28th International Conference on Software Engineering (ICSE 2006), Shanghai, China, May 20-28, 2006, pp. 873-876, 2006, ACM, 1-59593-375-1. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
static analysis, theorem proving, termination, liveness, ACL2 |
52 | David A. Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, Burkhart Wolff |
Verifying a signature architecture: a comparative case study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 19(1), pp. 63-91, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Security, Model checking, Formal methods, Theorem proving, Case study, Comparison |
51 | Herman Geuvers, Gueorgui I. Jojgov |
Open Proofs and Open Terms: A Basis for Interactive Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings, pp. 537-552, 2002, Springer, 3-540-44240-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
open terms, meta-variables, formulas-as-types, type theory, interactive theorem proving |
51 | Adel Bouhoula, Jean-Pierre Jouannaud |
Automata-Driven Automated Induction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pp. 14-25, 1997, IEEE Computer Society, 0-8186-7925-5. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
automata-driven automated induction, inductive theorem proving, first-order functions, finitely many unary membership predicates, rational subsets, ground reducibility, inductive prover, theorem proving, tree automata, Horn Clauses, proof obligations |
51 | Miriam Leeser, John W. O'Leary |
Verification of a subtractive radix-2 square root algorithm and implementation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCD ![In: 1995 International Conference on Computer Design (ICCD '95), VLSI in Computers and Processors, October 2-4, 1995, Austin, TX, USA, Proceedings, pp. 526-531, 1995, IEEE Computer Society, 0-8186-7165-3. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
subtractive radix-2 square root, floating point square root hardware, Intel Pentium, radix-2 square root, MIPS R4400, RTL level, verification, formal verification, theorem proving, theorem proving, floating point arithmetic, optimizing transformations |
51 | Zohar Manna, Richard J. Waldinger |
Fundamentals of Deductive Program Synthesis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 18(8), pp. 674-704, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
deductive program synthesis, deductive-tableau system, theorem-proving framework, nonclausal resolution rule, induction rule, formal specification, artificial intelligence, specification, theorem proving, program testing, reasoning, inference mechanisms, proof |
51 | Robert E. Fields, Morten Elvang-Gøransson |
A VDM Case Study in mural. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 18(4), pp. 279-295, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
interactive theorem-proving assistant, specification support tool, mural, verification, formal specification, specification, software tools, theorem proving, program verification, interactive systems, VDM, Vienna development method |
50 | Xiao-Shan Gao, Qiang Lin |
MMP/Geometer - A Software Package for Automated Geometric Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry, 4th International Workshop, ADG 2002, Hagenberg Castle, Austria, September 4-6, 2002, Revised Papers, pp. 44-66, 2002, Springer, 3-540-20927-1. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Geometry software, geometric theorem discovering, geometric diagram generation, intelligent dynamic geometry, automated reasoning, geometric theorem proving |
50 | Roope Kaivola, Mark D. Aagaard |
Divider Circuit Verification with Model Checking and Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 338-355, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
50 | Marta Franová |
Automated Inductive Reasoning as a Support of Deductive Reasoning in a User-Independent Automation of Inductive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMIS ![In: Foundations of Intelligent Systems, 9th International Symposium, ISMIS '96, Zakopane, Poland, June 9-13, 1996, Proceedings, pp. 551-560, 1996, Springer, 3-540-61286-6. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
49 | Michael Fisher 0001 |
Characterizing Simple Negotiation as Distributed Agent-Based Theorem-Proving - A Preliminary Report. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICMAS ![In: 4th International Conference on Multi-Agent Systems, ICMAS 2000, Boston, MA, USA, July 10-12, 2000, pp. 127-134, 2000, IEEE Computer Society, 0-7695-0625-9. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
49 | Pavel Vanousek |
Automated Theorem Proving in a Combination of Theories with Disjoint Signatures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SOFSEM ![In: SOFSEM '98: Theory and Practice of Informatics, 25th Conference on Current Trends in Theory and Practice of Informatics, Jasná, Slovakia, November 21-27, 1998, Proceedings, pp. 443-452, 1998, Springer, 3-540-65260-4. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
49 | Marta Franová |
Constructive Matching - Explanation Based Methodology for Inductive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IMYCS ![In: Aspects and Prospects of Theoretical Computer Science, 6th International Meeting of Young Computer Scientists, Smolenice, Czechoslovakia, November 19-23, 1990, Proceedings, pp. 138-147, 1990, Springer, 3-540-53414-8. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
49 | Larry Wos, William McCune |
Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 714-729, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
|
48 | Maria Paola Bonacina |
On theorem proving for program checking: historical perspective and recent developments. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 26-28, 2010, Hagenberg, Austria, pp. 1-12, 2010, ACM, 978-1-4503-0132-9. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
combination of theories, rewrite-based theorem proving, speculative inferences, satisfiability modulo theories |
48 | Chiyan Chen, Hongwei Xi |
Combining programming with theorem proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005, pp. 66-77, 2005, ACM, 1-59593-064-7. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
applied type system, proof erasure, theorem proving, dependent types, ATS |
48 | June Andronick, Boutheina Chetali, Olivier Ly |
Using Coq to Verify Java Card Applet Isolation Properties. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, pp. 335-351, 2003, Springer, 3-540-40664-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Security, Theorem Proving, Smart Card |
48 | Harald Ganzinger, Viorica Sofronie-Stokkermans |
Chaining Techniques for Automated Theorem Proving in Many-Valued Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMVL ![In: 30th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2000, Portland, Oregon, USA, May 23-25, 2000, Proceedings, pp. 337-344, 2000, IEEE Computer Society, 0-7695-0692-5. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
chaining calculi, resolution, many-valued logic, automated theorem proving, superposition |
48 | Viorica Sofronie-Stokkermans |
Representation Theorems and Theorem Proving in Non-Classical Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMVL ![In: 29th IEEE International Symposium on Multiple-Valued Logic, ISMVL 1999, Freiburg im Breisgau, Germany, May 20-22, 1999, Proceedings, pp. 242-247, 1999, IEEE Computer Society, 0-7695-0161-3. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
distributive lattices with operators, Priestley duality, many-values logics, automated theorem proving, Non-classical logics |
48 | Gernot Stenz, Andreas Wolf 0005 |
Scheduling Methods for Parallel Automated Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI ![In: Advances in Artificial Intelligence, 13th Biennial Conference of the Canadian Society for Computational Studies of Intelligence, AI 2000, Montréal, Quebec, Canada, May 14-17, 2000, Proceedings, pp. 254-266, 2000, Springer, 3-540-67557-4. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
47 | Xia Wu, Jigui Sun, Shuai Lu 0001, Ying Li, Wei Meng, Minghao Yin |
Improved Propositional Extension Rule. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RSKT ![In: Rough Sets and Knowledge Technology, First International Conference, RSKT 2006, Chongqing, China, July 24-26, 2006, Proceedings, pp. 592-597, 2006, Springer, 3-540-36297-5. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Extension rule, reduced rule, theorem proving, propositional logic |
47 | Sigrid Gürgens, Javier López 0001 |
Suitability of a Classical Analysis Method for E-commerce Protocols. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISC ![In: Information Security, 4th International Conference, ISC 2001, Malaga, Spain, October 1-3, 2001, Proceedings, pp. 46-62, 2001, Springer, 3-540-42662-0. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
electronic commerce, cryptographic protocol, Security analysis, automatic theorem proving, protocol validation |
47 | Mark D. Aagaard, Carl-Johan H. Seger |
The formal verification of a pipelined double-precision IEEE floating-point multiplier. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCAD ![In: Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1995, San Jose, California, USA, November 5-9, 1995, pp. 7-10, 1995, IEEE Computer Society / ACM, 0-8186-7213-7. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
ANSI/IEEE Std 754-1985, model checking, theorem proving, floating-point arithmetic, Hardware verification |
47 | Li Dafa |
An Application to Teaching in Logic Course of ATP Based Natural Deduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, pp. 463-465, 1992, Springer, 3-540-55727-X. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
theorem proving, logic, natural deduction |
46 | Anduo Wang, Prithwish Basu, Boon Thau Loo, Oleg Sokolsky |
Declarative Network Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PADL ![In: Practical Aspects of Declarative Languages, 11th International Symposium, PADL 2009, Savannah, GA, USA, January 19-20, 2009. Proceedings, pp. 61-75, 2009, Springer, 978-3-540-92994-9. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
network protocol verification, theorem proving, domain-specific languages, Declarative networking |
46 | Haiyan Xiong, Paul Curzon, Sofiène Tahar, Ann Blandford |
Formally Linking MDG and HOL Based on a Verified MDG System. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFM ![In: Integrated Formal Methods, Third International Conference, IFM 2002, Turku, Finland, May 15-18, 2002, Proceedings, pp. 205-224, 2002, Springer, 3-540-43703-7. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
hybrid verification systems, deductive theorem proving, symbolic state enumeration, usability verification, hardware verification |
46 | B. Kutzler |
Careful Algebraic Translations of Geometry Theorems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSAC ![In: Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC '89, Portland, Oregon, USA, July 17-19, 1989, pp. 254-263, 1989, ACM, 0-89791-325-6. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
computational analytical geometry, automated geometry theorem proving |
46 | César A. Muñoz, David R. Lester |
Real Number Calculations and Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 195-210, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
46 | Konrad Slind, Joe Hurd |
Applications of Polytypism in Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, pp. 103-119, 2003, Springer, 3-540-40664-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
46 | Simon Ambler, Roy L. Crole, Alberto Momigliano |
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 13-30, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
46 | François Puitg, Jean-François Dufourd |
Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, pp. 401-422, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
45 | Devrim Unal, M. Ufuk Çaglayan |
Theorem proving for modeling and conflict checking of authorization policies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISCN ![In: Proceedings of the International Symposium on Computer Networks, ISCN 2006, June 16-18, 2006, Istanbul, Turkey, pp. 146-151, 2006, IEEE. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
45 | Christian Jacobi 0002 |
Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, pp. 309-323, 2002, Springer, 3-540-43997-8. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
45 | Michael J. C. Gordon |
PuzzleTool : An Example of Programming Computation and Deduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 214-229, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
45 | Carl-Johan H. Seger |
Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, pp. 235, 2000, Springer, 3-540-67664-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
45 | Andreas Franke 0001, Michael Kohlhase |
System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, pp. 217-221, 1999, Springer, 3-540-66222-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
45 | Anna Mikhajlova, Joakim von Wright |
Proving Isomorphism of First-Order Logic Proof Systems in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, pp. 295-314, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
45 | Ewing L. Lusk |
Controlling Redundancy in Large Search Spaces: Argonne-Style Theorem Proving Through the Years. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, pp. 96-106, 1992, Springer, 3-540-55727-X. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
45 | Ross A. Overbeek, Ewing L. Lusk |
Data Structures and Control Architectures for Implementation of Theorem-Proving Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings, pp. 232-249, 1980, Springer, 3-540-10009-1. The full citation details ...](Pics/full.jpeg) |
1980 |
DBLP DOI BibTeX RDF |
|
45 | Larry Wos, George A. Robinson, Daniel F. Carson, Leon Shalla |
The Concept of Demodulation in Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 14(4), pp. 698-709, 1967. The full citation details ...](Pics/full.jpeg) |
1967 |
DBLP DOI BibTeX RDF |
|
45 | Ching-Tsun Chou |
A Note on Interactive Theorem Proving with Theorem Continuation Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992, pp. 59-69, 1992, North-Holland/Elsevier, 0-444-89880-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
43 | Li Dafa |
Intelligent CAI Course in the First-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCAL ![In: Computer Assisted Learning, 3rd International Conference, ICCAL '90, Hagen, FRG, June 11-13, 1990, Proceedings, pp. 67-72, 1990, Springer, 3-540-52699-4. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
tautology, theorem proving, first-order logic, resolution, natural deduction |
43 | Vlad Rusu, Eli Singerman |
On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS '99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings, pp. 178-192, 1999, Springer, 3-540-65703-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
42 | Monty Newborn, Zongyan Wang |
Octopus: Combining Learning and Parallel Search. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 33(2), pp. 171-218, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
Octopus, TPTP, automated theorem proving, learning strategies, parallel search |
42 | Ben L. Di Vito |
High-automation proofs for properties of requirements models. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 3(1), pp. 20-31, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Avionics software, Proof strategies, Formal methods, Theorem proving, Requirements analysis |
42 | Rajeev Goré, Lan Duy Nguyen |
CardKt: Automated Multi-modal Deduction on Java Cards for Multi-application Security. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Java Card Workshop ![In: Java on Smart Cards: Programming and Security, First International Workshop, JavaCard 2000, Cannes, France, September 14, 2000, Revised Papers, pp. 38-51, 2000, Springer, 3-540-42167-X. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
security of multi-application smart cards, applications of logics of knowledge and belief, modal theorem proving, tense logics |
42 | Andrew Ireland, Mike Jackson 0003, Gordon Reid |
Interactive Proof Critics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 11(3), pp. 302-325, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
Proof patching, Inductive proof, User interfaces, Theorem proving, Proof planning |
42 | Randall W. Lichota, Grace L. Hammonds, Stephen H. Brackin |
Verifying The Correctness Of Cryptographic Protocols Using "Convince". ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACSAC ![In: 12th Annual Computer Security Applications Conference (ACSAC 1996), 9-13 December 1996, San Diego, CA, USA, pp. 117-128, 1996, IEEE Computer Society. The full citation details ...](Pics/full.jpeg) |
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 |
42 | Serge Autexier, Dieter Hutter, Bruno Langenstein, Heiko Mantel, Georg Rock, Axel Schairer, Werner Stephan 0001, Roland Vogt, Andreas Wolpers |
VSE: formal methods meet industrial needs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 3(1), pp. 66-77, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Formal software development, Modular proof development, Temporal logic, Compositionality, Automated theorem proving, Interactive theorem proving |
42 | F. Keith Hanna, Neil Daeche, Mark Longley |
Specification and Verification Using Dependent Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 16(9), pp. 949-964, 1990. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
VERITAS/sup +/, iterative structures, functional metalanguage, computational implementation, modeling, modelling, formal specification, theorem proving, theorem proving, iterative methods, dependent types, numerals, specification logic |
41 | Noboru Matsuda, Kurt VanLehn |
Modeling Hinting Strategies for Geometry Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
User Modeling ![In: User Modeling 2003, 9th International Conference, UM 2003, Johnstown, PA, USA, June 22-26, 2003, Proceedings, pp. 373-377, 2003, Springer, 3-540-40381-7. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
40 | In-Hee Lee, Ji-Yoon Park, Hae-Man Jang, Young-Gyu Chai, Byoung-Tak Zhang |
DNA Implementation of Theorem Proving with Resolution Refutation in Propositional Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DNA ![In: DNA Computing, 8th International Workshop on DNA Based Computers, DNA8, Sapporo, Japan, June 10-13, 2002, Revised Papers, pp. 156-167, 2002, Springer, 3-540-00531-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
40 | Chad E. Brown |
Solving for Set Variables in Higher-Order Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, pp. 408-422, 2002, Springer, 3-540-43931-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
40 | Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea |
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, pp. 438-455, 2002, Springer, 3-540-43931-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
40 | Noboru Matsuda, Kurt VanLehn |
A Reification of a Strategy for Geometry Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Intelligent Tutoring Systems ![In: Intelligent Tutoring Systems, 5th International Conference, ITS 2000, Montréal, Canada, June 19-23, 2000, Proceedings, pp. 660, 2000, Springer, 3-540-67655-4. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
40 | Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers |
Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 11th International Conference, CAV '99, Trento, Italy, July 6-10, 1999, Proceedings, pp. 369-379, 1999, Springer, 3-540-66202-2. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
40 | Dirk Fuchs |
Requirement-Based Cooperative Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in Artificial Intelligence, European Workshop, JELIA '98, Dagstuhl, Germany, October 12-15, 1998, Proceedings, pp. 139-153, 1998, Springer, 3-540-65141-1. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
40 | Leo Bachmair, Harald Ganzinger, Uwe Waldmann |
Theorem Proving for Hierarchic First-Order Theories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ALP ![In: Algebraic and Logic Programming, Third International Conference, Volterra, Italy, September 2-4, 1992, Proceedings, pp. 420-434, 1992, Springer, 3-540-55873-X. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
40 | Heikki Tuominen |
Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 514-527, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
40 | David Y. Y. Yun, Y. Yun, Chang Nian Zhang |
Formal verification of systolic networks using theorem proving techniques (abstract only). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Conference on Computer Science ![In: Proceedings of the 15th ACM Annual Conference on Computer Science, St. Louis, Missouri, USA, February 16-19, 1987, pp. 362, 1987, ACM, 0-89791-218-7. The full citation details ...](Pics/full.jpeg) |
1987 |
DBLP DOI BibTeX RDF |
|
40 | Osman Hasan, Sofiène Tahar, Naeem Abbasi |
Formal Reliability Analysis Using Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 59(5), pp. 579-592, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
theorem proving, Formal models, memory structures, performance and reliability |
40 | Karl-Heinz Pennemann |
Resolution-Like Theorem Proving for High-Level Conditions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICGT ![In: Graph Transformations, 4th International Conference, ICGT 2008, Leicester, United Kingdom, September 7-13, 2008. Proceedings, pp. 289-304, 2008, Springer, 978-3-540-87404-1. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
first-order tautology problem, high-level conditions, weak adhesive HLR categories, theorem proving, resolution |
40 | Steven P. Miller |
Will This Be Formal? ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 6-11, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
model checking, Formal methods, theorem proving, avionics |
40 | Ghiath Al Sammane, Julien Schmaltz, Diana Toma, Pierre Ostier, Dominique Borrione |
TheoSim: combining symbolic simulation and theorem proving for hardware verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBCCI ![In: Proceedings of the 17th Annual Symposium on Integrated Circuits and Systems Design, SBCCI 2004, Pernambuco, Brazil, September 7-11, 2004, pp. 60-65, 2004, ACM. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
theorem proving, symbolic simulation, hardware verification |
40 | Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin |
Specification and Verification of a Steam-Boiler with Signal-Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 356-371, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
the steam-boiler problem, theorem proving, synchronous programming |
40 | Keith Vanderveen, C. V. Ramamoorthy |
Partial instantiation theorem proving for distributed resource location. ![Search on Bibsonomy](Pics/bibsonomy.png) |
COMPSAC ![In: 21st International Computer Software and Applications Conference (COMPSAC '97), 11-15 August 1997, Washington, DC, USA, pp. 192-197, 1997, IEEE Computer Society, 0-8186-8105-5. The full citation details ...](Pics/full.jpeg) |
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 |
40 | David Cyrluk, Mandayam K. Srivas |
Theorem proving: not an esoteric diversion, but the unifying framework for industrial verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCD ![In: 1995 International Conference on Computer Design (ICCD '95), VLSI in Computers and Processors, October 2-4, 1995, Austin, TX, USA, Proceedings, pp. 538-544, 1995, IEEE Computer Society, 0-8186-7165-3. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
industrial hardware verification, industrial verification, formal verification, logic testing, theorem proving, theorem prover, hardware verification |
40 | Jean H. Gallier, Paliath Narendran, Stan Raatz, Wayne Snyder |
Theorem Proving Using Equational Matings and Rigid E-Unification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 39(2), pp. 377-429, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
Knuth-Bendix procedure, matings, NP-completeness, unification, automated theorem proving, equational reasoning |
40 | Wolfgang Ertel |
OR-Parallel Theorem Proving with Random Competition. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, pp. 226-237, 1992, Springer, 3-540-55727-X. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
random competition, SETHEO, theorem proving, speedup, OR-parallelism, random search, model elimination |
40 | Oliver Bittel |
Tableau-Based Theorem Proving and Synthesis of Lambda-Terms in the Intuitionistic Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in AI, European Workshop, JELIA '92, Berlin, Germany, September 7-10, 1992, Proceedings, pp. 262-278, 1992, Springer, 3-540-55887-X. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
Typed -Calculus, Program Synthesis, Intuitionistic Logic, Automatic Theorem Proving |
40 | Shang-Ching Chou, Xiao-Shan Gao |
Ritt-Wu's Decomposition Algorithm and Geometry Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 207-220, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
Wu's method, prover, elementary geometry, degenerate conditions, Ritt-Wu's principle, ascending chain, the dimension theorem, Morley's trisector theorem, ideal, mechanical theorem proving, algebraic variety |
40 | Waldo C. Kabat, Anthony S. Wojcik |
Automated Synthesis of Combinational Logic Using Theorem-Proving Techniques. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 34(7), pp. 610-632, 1985. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
logic design, multivalued logic, design automation, Automated theorem proving, switching theory |
40 | Witold S. Wojciechowski, Anthony S. Wojcik |
Automated Design of Multiple-Valued Logic Circuits by Automatic Theorem Proving Techniques. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 32(9), pp. 785-798, 1983. The full citation details ...](Pics/full.jpeg) |
1983 |
DBLP DOI BibTeX RDF |
multiple-valued circuits, theorem proving, logic design, first order logic, Automated design, formal proof |
40 | John D. McCharen, Ross A. Overbeek, Larry Wos |
Problems and Experiments for and with Automated Theorem-Proving Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Computers ![In: IEEE Trans. Computers 25(8), pp. 773-782, 1976. The full citation details ...](Pics/full.jpeg) |
1976 |
DBLP DOI BibTeX RDF |
Clause sets, UR resolution, theorem-proving, resolution |
Displaying result #1 - #100 of 3383 (100 per page; Change: ) Pages: [ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ >>] |
|