|
|
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. |
ISICA |
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. |
IEEE Des. Test Comput. |
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. |
ACM Conference on Computer Science |
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. |
ACM Great Lakes Symposium on VLSI |
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. |
RTA |
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. |
HUG |
1993 |
DBLP DOI BibTeX RDF |
|
66 | Wing-Kwong Wong, Bo-Yu Chan, Sheng-Kai Yin |
A Dynamic Geometry Environment for Learning Theorem Proving. |
ICALT |
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. |
Automated Deduction in Geometry |
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. |
ECBS |
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. |
Int. J. Softw. Tools Technol. Transf. |
2000 |
DBLP DOI BibTeX RDF |
Formal methods, Mechanized theorem proving |
65 | Jieh Hsiang, Mandayam K. Srivas |
PROLOG-Based Inductive Theorem Proving. |
FSTTCS |
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. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
62 | Larry Wos |
Solving Open Questions with an Automated Theorem-Proving Program. |
CADE |
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. |
APSEC |
2005 |
DBLP DOI BibTeX RDF |
|
61 | Chih-Hung Wu, Shie-Jue Lee |
On parallelism of hyper-linking theorem proving: a preliminary report. |
ICPADS |
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. |
IEEE Trans. Knowl. Data Eng. |
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. |
J. Comput. Sci. Technol. |
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. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
58 | David R. Lester |
Real Number Calculations and Theorem Proving. |
TPHOLs |
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. |
IUI |
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. |
J. Autom. Reason. |
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. |
J. Autom. Reason. |
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. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
semantics, Types, pi calculus, automatic theorem proving |
56 | David A. Plaisted |
Special Cases and Substitutes for Rigid E-Unification. |
Appl. Algebra Eng. Commun. Comput. |
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. |
Mechanizing Mathematical Reasoning |
2005 |
DBLP DOI BibTeX RDF |
|
54 | Helko Lehmann, Michael Leuschel |
Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce. |
LOPSTR |
2003 |
DBLP DOI BibTeX RDF |
|
52 | Panagiotis Manolios, Daron Vroon 0001 |
Integrating static analysis and general-purpose theorem proving for termination analysis. |
ICSE |
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. |
Formal Aspects Comput. |
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. |
CSL |
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. |
LICS |
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. |
ICCD |
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. |
IEEE Trans. Software Eng. |
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. |
IEEE Trans. Software Eng. |
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. |
Automated Deduction in Geometry |
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. |
TPHOLs |
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. |
ISMIS |
1996 |
DBLP DOI BibTeX RDF |
|
49 | Michael Fisher 0001 |
Characterizing Simple Negotiation as Distributed Agent-Based Theorem-Proving - A Preliminary Report. |
ICMAS |
2000 |
DBLP DOI BibTeX RDF |
|
49 | Pavel Vanousek |
Automated Theorem Proving in a Combination of Theories with Disjoint Signatures. |
SOFSEM |
1998 |
DBLP DOI BibTeX RDF |
|
49 | Marta Franová |
Constructive Matching - Explanation Based Methodology for Inductive Theorem Proving. |
IMYCS |
1990 |
DBLP DOI BibTeX RDF |
|
49 | Larry Wos, William McCune |
Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. |
CADE |
1988 |
DBLP DOI BibTeX RDF |
|
48 | Maria Paola Bonacina |
On theorem proving for program checking: historical perspective and recent developments. |
PPDP |
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. |
ICFP |
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. |
TPHOLs |
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. |
ISMVL |
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. |
ISMVL |
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. |
AI |
2000 |
DBLP DOI BibTeX RDF |
|
47 | Xia Wu, Jigui Sun, Shuai Lu 0001, Ying Li, Wei Meng, Minghao Yin |
Improved Propositional Extension Rule. |
RSKT |
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. |
ISC |
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. |
ICCAD |
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. |
LPAR |
1992 |
DBLP DOI BibTeX RDF |
theorem proving, logic, natural deduction |
46 | Anduo Wang, Prithwish Basu, Boon Thau Loo, Oleg Sokolsky |
Declarative Network Verification. |
PADL |
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. |
IFM |
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. |
ISSAC |
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. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
46 | Konrad Slind, Joe Hurd |
Applications of Polytypism in Theorem Proving. |
TPHOLs |
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. |
TPHOLs |
2002 |
DBLP DOI BibTeX RDF |
|
46 | François Puitg, Jean-François Dufourd |
Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
45 | Devrim Unal, M. Ufuk Çaglayan |
Theorem proving for modeling and conflict checking of authorization policies. |
ISCN |
2006 |
DBLP DOI BibTeX RDF |
|
45 | Christian Jacobi 0002 |
Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
45 | Michael J. C. Gordon |
PuzzleTool : An Example of Programming Computation and Deduction. |
TPHOLs |
2002 |
DBLP DOI BibTeX RDF |
|
45 | Carl-Johan H. Seger |
Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
45 | Andreas Franke 0001, Michael Kohlhase |
System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving. |
CADE |
1999 |
DBLP DOI BibTeX RDF |
|
45 | Anna Mikhajlova, Joakim von Wright |
Proving Isomorphism of First-Order Logic Proof Systems in HOL. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
45 | Ewing L. Lusk |
Controlling Redundancy in Large Search Spaces: Argonne-Style Theorem Proving Through the Years. |
LPAR |
1992 |
DBLP DOI BibTeX RDF |
|
45 | Ross A. Overbeek, Ewing L. Lusk |
Data Structures and Control Architectures for Implementation of Theorem-Proving Programs. |
CADE |
1980 |
DBLP DOI BibTeX RDF |
|
45 | Larry Wos, George A. Robinson, Daniel F. Carson, Leon Shalla |
The Concept of Demodulation in Theorem Proving. |
J. ACM |
1967 |
DBLP DOI BibTeX RDF |
|
45 | Ching-Tsun Chou |
A Note on Interactive Theorem Proving with Theorem Continuation Functions. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
43 | Li Dafa |
Intelligent CAI Course in the First-Order Logic. |
ICCAL |
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. |
TACAS |
1999 |
DBLP DOI BibTeX RDF |
|
42 | Monty Newborn, Zongyan Wang |
Octopus: Combining Learning and Parallel Search. |
J. Autom. Reason. |
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. |
Int. J. Softw. Tools Technol. Transf. |
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. |
Java Card Workshop |
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. |
Formal Aspects Comput. |
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". |
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 |
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. |
Int. J. Softw. Tools Technol. Transf. |
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. |
IEEE Trans. Software Eng. |
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. |
User Modeling |
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. |
DNA |
2002 |
DBLP DOI BibTeX RDF |
|
40 | Chad E. Brown |
Solving for Set Variables in Higher-Order Theorem Proving. |
CADE |
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. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
40 | Noboru Matsuda, Kurt VanLehn |
A Reification of a Strategy for Geometry Theorem Proving. |
Intelligent Tutoring Systems |
2000 |
DBLP DOI BibTeX RDF |
|
40 | Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers |
Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
40 | Dirk Fuchs |
Requirement-Based Cooperative Theorem Proving. |
JELIA |
1998 |
DBLP DOI BibTeX RDF |
|
40 | Leo Bachmair, Harald Ganzinger, Uwe Waldmann |
Theorem Proving for Hierarchic First-Order Theories. |
ALP |
1992 |
DBLP DOI BibTeX RDF |
|
40 | Heikki Tuominen |
Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic. |
CADE |
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). |
ACM Conference on Computer Science |
1987 |
DBLP DOI BibTeX RDF |
|
40 | Osman Hasan, Sofiène Tahar, Naeem Abbasi |
Formal Reliability Analysis Using Theorem Proving. |
IEEE Trans. Computers |
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. |
ICGT |
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? |
TPHOLs |
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. |
SBCCI |
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. |
TPHOLs |
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. |
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 |
40 | 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 |
40 | Jean H. Gallier, Paliath Narendran, Stan Raatz, Wayne Snyder |
Theorem Proving Using Equational Matings and Rigid E-Unification. |
J. ACM |
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. |
LPAR |
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. |
JELIA |
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. |
CADE |
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. |
IEEE Trans. Computers |
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. |
IEEE Trans. Computers |
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. |
IEEE Trans. Computers |
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][ >>] |
|