Search results for "theorem"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
78	Alexej P. Pynko	A relative interpolation theorem for infinitary universal Horn logic and its applications.	Arch. Math. Log.	2006	DBLP DOI BibTeX RDF	Universal Horn theory, Interpolation theorem, Preservation theorem, Definability theorem
62	Lai-Jiu Lin 0001, Wei-Shih Du	Systems of equilibrium problems with applications to new variants of Ekeland's variational principle, fixed point theorems and parametric optimization problems.	J. Glob. Optim.	2008	DBLP DOI BibTeX RDF	?-function, Quasi-distance, Ekeland’s variational principle, Flower petal theorem, Maximal element theorem, Minimax theorem, Minimization theorem, Semi-infinite problem, Generalized Schauder’s fixed point theorem, Equilibrium problem
50	Mihaly Agfalvi, Istvan Kadar, Erik Papp	Generalization of Pick's theorem for surface of polyhedra.	APL	1999	DBLP DOI BibTeX RDF	APL
50	Hiroyuki Honda, Miki Haseyama, Hideo Kitajima, S. Matsumoto	Extension of the Collage Theorem.	ICIP (2)	1997	DBLP DOI BibTeX RDF	collage theorem, fractal image compression, extended collage theorem, IFS algorithm, contraction mappings, data compression, quality, errors, iteration, iterative function system, reconstructed image
47	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
41	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
41	Ken-ichi Kawarabayashi, Bruce A. Reed	Hadwiger's conjecture is decidable.	STOC	2009	DBLP DOI BibTeX RDF	Hadwiger's conjecture, the four color theorem
39	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
38	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
38	Christian Pech	Kleene's Theorem for Weighted Tree-Automata.	FCT	2003	DBLP DOI BibTeX RDF	Kleenes theorem, Schützenbergers theorem, rational expression, tree, language, automata, weight
36	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
35	Vasco Brattka	Borel complexity and computability of the Hahn-Banach Theorem.	Arch. Math. Log.	2008	DBLP DOI BibTeX RDF	Mathematics Subject Classification (2000) 03F60, 46S30, 03E15
35	Gianni Bosi, Gerhard Herden	On a Possible Continuous Analogue of the Szpilrajn Theorem and its Strengthening by Dushnik and Miller.	Order	2006	DBLP DOI BibTeX RDF	Mathematics Subject Classifications (2000) 54F05, 06A05, 91B16
35	Shang-Ching Chou	A Geometry Theorem Prover for Macintoshes.	CADE	1992	DBLP DOI BibTeX RDF
35	Maria Paola Bonacina, Jieh Hsiang	On Fairness of Completion-Based Theorem Proving Strategies.	RTA	1991	DBLP DOI BibTeX RDF
35	Jieh Hsiang, Mandayam K. Srivas	PROLOG-Based Inductive Theorem Proving.	FSTTCS	1985	DBLP DOI BibTeX RDF
34	Micha A. Perles, Horst Martini, Yaakov S. Kupitz	A Jordan-Brouwer Separation Theorem for Polyhedral Pseudomanifolds.	Discret. Comput. Geom.	2009	DBLP DOI BibTeX RDF	Bing’s house, Euler’s formula, Jordan-Brouwer theorem, Jordan’s curve theorem, Jordan exterior (interior), Polygonal diameter, Polyhedral manifold, Triangulation, Dual graph
32	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
32	Daniel Fridlender	An Interpretation of the Fan Theorem in Type Theory.	TYPES	1998	DBLP DOI BibTeX RDF	fan theorem, inductive bar, type theory
32	Thomas H. Reiss	The revised Fundamental Theorem of Moment Invariants.	IEEE Trans. Pattern Anal. Mach. Intell.	1991	DBLP DOI BibTeX RDF	fundamental theorem, similitude, general linear transformations, pattern recognition, pattern recognition, invariance, invariance, algebra, algebra, rotation invariants, moment invariants
32	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
32	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
32	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
31	Yunnan Wu, Kamal Jain, Sun-Yuan Kung	A unification of network coding and tree-packing (routing) theorems.	IEEE Trans. Inf. Theory	2006	DBLP DOI BibTeX RDF	routing, multicast, network coding, steiner tree, flow
31	Irit Dinur	The PCP theorem by gap amplification.	J. ACM	2007	DBLP DOI BibTeX RDF	Gap amplification, PCP
31	Gianni Bosi, Gerhard Herden	On a Strong Continuous Analogue of the Szpilrajn Theorem and its Strengthening by Dushnik and Miller.	Order	2005	DBLP DOI BibTeX RDF	Mathematics Subject Classification (2000) 54F05, 06A05, 91B16
31	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
31	Zdzislaw Pawlak	The Rough Set View on Bayes' Theorem.	AFSS	2002	DBLP DOI BibTeX RDF
31	Yun Wang, Yanyong Guan, Hongkai Wang, Kaiquan Shi	An Improved Intermediate Value Theorem and Rough Fix-Point Theorem of Roughly Continuous Discrete Functions.	FSKD (5)	2008	DBLP DOI BibTeX RDF
31	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
30	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
30	Marc Bezem, Dimitri Hendriks	On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Coherent logic, Proof objects, Hessenberg’s theorem, Automated theorem proving
30	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
30	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
30	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
30	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
30	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
29	Katarína Cunderlíková	The individual ergodic theorem on the IF-events with product.	Soft Comput.	2010	DBLP DOI BibTeX RDF	The IF-event, The IF-probability, The IF-observable, The product, The upper and lower limits, The individual ergodic theorem, The almost everywhere convergence, The -preserving transformation
29	Olga Brezhneva, Alexey Tret'yakov, Stephen E. Wright	A simple and elementary proof of the Karush-Kuhn-Tucker theorem for inequality-constrained optimization.	Optim. Lett.	2009	DBLP DOI BibTeX RDF	Karush-Kuhn-Tucker theorem, Nonlinear programming
29	Jean-François Dufourd	An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Computer-aided proofs, Coq system, Combinatorial hypermaps, Discrete Jordan Curve Theorem, Formal specifications, Computational topology, Planar subdivisions
29	Akimasa Morihata, Kiminori Matsuzaki, Zhenjiang Hu, Masato Takeichi	The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer.	POPL	2009	DBLP DOI BibTeX RDF	huet's zippers, polynomial data structures, the third homomorphism theorem, divide-and-conquer
29	Gilbert Labelle, Annie Lacasse	Discrete Versions of Stokes' Theorem Based on Families of Weights on Hypercubes.	DGCI	2009	DBLP DOI BibTeX RDF	Discrete Stokes’ theorem, Poincaré lemma, hypercube
29	Antoni Torrens	An Approach to Glivenko's Theorem in Algebraizable Logics.	Stud Logica	2008	DBLP DOI BibTeX RDF	Glivenko’s Theorem, equivalential deductive system, compatible expansion, algebraic semantics, quasivariety, algebraizable logic
29	Satyadev Nandakumar	An effective ergodic theorem and some applications.	STOC	2008	DBLP DOI BibTeX RDF	ergodic theorem, algorithmic randomness
29	Josef Berger	The Logical Strength of the Uniform Continuity Theorem.	CiE	2006	DBLP DOI BibTeX RDF	Constructive reverse mathematics, uniform continuity theorem
29	Victoria Powers, Bruce Reznick	A quantitative Pólya's Theorem with corner zeros.	ISSAC	2006	DBLP DOI BibTeX RDF	Pólya's Theorem, positive polynomials, sums of squares
29	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
29	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
29	Hongbo Li 0012, Ronghua Xu, Ning Zhang	On Miquel's Five-Circle Theorem.	IWMM/GIAE	2004	DBLP DOI BibTeX RDF	Miquel’s Theorem, Mathematics mechanization, Null bracket algebra, “breefs”, Conformal geometric algebra
29	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
29	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
29	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
29	Werner Schindler	A Timing Attack against RSA with the Chinese Remainder Theorem.	CHES	2000	DBLP DOI BibTeX RDF	RSA, Chinese Remainder Theorem, Montgomery multiplication, Timing attack
29	Piergiorgio Bertoli, Jacques Calmet, Fausto Giunchiglia, Karsten Homann	Specification and Integration of Theorem Provers and Computer Algebra Systems.	AISC	1998	DBLP DOI BibTeX RDF	Integration, Theorem Provers, Computer Algebra Systems, Formal Frameworks
29	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
29	Jianan Li, Ichiro Suzuki, Masafumi Yamashita	A New Structural Induction Theorem for Rings of Temporal Petri Nets.	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	structural induction theorem, temporal Petri nets, identical components, temporal logic formula, similar behavior, demand-driven token circulation, Petri nets, formal verification, formal verification, temporal logic, correctness, temporal reasoning, rings
29	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
28	Stephen Simons	Minimax Theorems.	Encyclopedia of Optimization	2009	DBLP DOI BibTeX RDF	Minimax theorem, Hahn-Banach theorem, Connectedness, Fixed point theorem
28	Anna Avallone, Paolo Vitolo	Effect algebras with the subsequential interpolation property.	Soft Comput.	2008	DBLP DOI BibTeX RDF	Subsequential interpolation, Vitali-Hahn-Saks theorem, Brooks-Jewett theorem, Nikodym boundedness theorem, property, Effect algebras
27	Daniele Micciancio, Saurabh Panjwani	Adaptive Security of Symbolic Encryption.	TCC	2005	DBLP DOI BibTeX RDF
27	Alexander Leitsch	Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction.	FTP (LNCS Selection)	1998	DBLP DOI BibTeX RDF
27	Ian Horrocks 0001, Andrei Voronkov	Reasoning Support for Expressive Ontology Languages Using a Theorem Prover.	FoIKS	2006	DBLP DOI BibTeX RDF
27	Rongde Lu, An Lu	Applications of the Superposition Theorem to Nonlinear Resistive Circuits.	APCCAS	2006	DBLP DOI BibTeX RDF
27	Till Tantau	Towards a Cardinality Theorem for Finite Automata.	MFCS	2002	DBLP DOI BibTeX RDF
27	Imre Bárány, Gyula Károlyi	Problems and Results around the Erdös-Szekeres Convex Polygon Theorem.	JCDCG	2000	DBLP DOI BibTeX RDF
27	Gernot Stenz, Andreas Wolf 0005	Scheduling Methods for Parallel Automated Theorem Proving.	AI	2000	DBLP DOI BibTeX RDF
27	Jörg Desel	A Proof of the Rank Theorem for Extended Free Choice Nets.	Application and Theory of Petri Nets	1992	DBLP DOI BibTeX RDF	free choice nets - analysis, structure and behaviour of nets
27	Larry Wos	Solving Open Questions with an Automated Theorem-Proving Program.	CADE	1982	DBLP DOI BibTeX RDF
27	Bernard A. Galler, D. P. Rozenberg	A Generalization of a Theorem of Carr on Error Bounds for Rung-Kutta Procedures.	J. ACM	1960	DBLP DOI BibTeX RDF
27	Nobuyuki Sakamoto, Keita Yokoyama	The Jordan curve theorem and the Schönflies theorem in weak second-order arithmetic.	Arch. Math. Log.	2007	DBLP DOI BibTeX RDF	Mathematics Subject Classification (2000) Primary 03B30, Secondary 03F35, 26E35
27	Radomir S. Stankovic, Jaakko Astola	Reading the Sampling Theorem in Multiple-Valued Logic: A Journey from the (Shannong) Sampling Theorem to the Shannon Decomposition Rule.	ISMVL	2007	DBLP DOI BibTeX RDF
27	Chun Zhao, Ping Zhao 0004	Sampling theorem and irregular sampling theorem for multiwavelet subspaces.	IEEE Trans. Signal Process.	2005	DBLP DOI BibTeX RDF
27	R. E. Hodel	Restricted versions of the Tukey-Teichmüller theorem that are equivalent to the Boolean prime ideal theorem.	Arch. Math. Log.	2005	DBLP DOI BibTeX RDF
27	Ruben Gamboa, John R. Cowles	A Mechanical Proof of the Cook-Levin Theorem.	TPHOLs	2004	DBLP DOI BibTeX RDF
27	Christophe Dehlinger, Jean-François Dufourd	Formalizing the Trading Theorem for the Classification of Surfaces.	TPHOLs	2002	DBLP DOI BibTeX RDF
27	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
27	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
26	Yves Bertot, Vladimir Komendantsky	Fixed point semantics and partial recursion in Coq.	PPDP	2008	DBLP DOI BibTeX RDF	least fixed point semantics, non-terminating functions, program extraction, the Knaster-Tarski theorem, automated theorem proving
26	Guillaume Bonfante, Matthieu Kaczmarek, Jean-Yves Marion	A Classification of Viruses Through Recursion Theorems.	CiE	2007	DBLP DOI BibTeX RDF	iteration theorem, polymorphism, propagation, Computer viruses, recursion theorem
26	Gunther Schmidt 0001	Homomorphism and Isomorphism Theorems Generalized from a Relational Perspective.	RelMiCS	2006	DBLP DOI BibTeX RDF	homomorphism theorem, isomorphism theorem, multi-covering, relation algebra, congruence
26	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
26	Zengtai Gong, Yabin Shao	The Decomposition and Representation Theorem of Rough Fuzzy Set.	ISIP	2008	DBLP DOI BibTeX RDF	Nested sets, Representation theorem, Rough fuzzy set, Decomposition theorem
26	Jen-Ho Yang, Chin-Chen Chang 0001	Aryabhata Remainder Theorem for Moduli with Common Factors and Its Application in Information Protection Systems.	IIH-MSP	2008	DBLP DOI BibTeX RDF	Aryabhata Remainder Theorem, Information Protection Systems, Chinese Remainder Theorem
26	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
26	A. Wolinsky	A simple proof of Lewin's ordered-retrieval theorem for associative memories.	Commun. ACM	1968	DBLP DOI BibTeX RDF	access frequency proof, column digit values, column sensing arrangement, digit value readout, digit value variety, digit variety readout, memory access frequency, ordered information retrieval, ordered lists, ordered retrieval efficiency, ordered retrieval theorem, retrieval theorem proof, associative memories, content-addressed memories, memory access
25	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
25	Giulio Manzonetto, Antonino Salibra	From lambda-Calculus to Universal Algebra and Back.	MFCS	2008	DBLP DOI BibTeX RDF	Church Algebras, Stone Representation Theorem, Lambda Theories, Lambda calculus, Universal Algebra
25	Antonio Di Nola, Mirko Navara	MV-Algebras with the Cantor-Bernstein Property.	IFSA (2)	2007	DBLP DOI BibTeX RDF	Cantor-Bernstein theorem, boolean element of an MV-algebra, partition of unity, direct product decomposition, ?-complete MV-algebra, multiplicative MV-algebra, MV-algebra
25	Ren Ng	Fourier slice photography.	ACM Trans. Graph.	2005	DBLP DOI BibTeX RDF	digital refocusing, plenoptic camera, projection-slice theorem, fourier transform, digital photography
25	Kenichiro Tanabe	A Criterion for Designs in {\tf="P101461" Z}_4-codes on the Symmetrized Weight Enumerator.	Des. Codes Cryptogr.	2003	DBLP DOI BibTeX RDF	Z 4-codes, Assmus-Mattson theorem, harmonic weight, enumerator
25	Yair Bartal, Nathan Linial, Manor Mendel, Assaf Naor	On metric ramsey-type phenomena.	STOC	2003	DBLP DOI BibTeX RDF	Dvoretzky theorem, Ramsey theory, finite metric spaces
25	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
25	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
25	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
25	Clemens Ballarin, Lawrence C. Paulson	Reasoning About Coding Theory: The Benefits We Get from Computer Algebra.	AISC	1998	DBLP DOI BibTeX RDF	mechanised reasoning, combining systems, soundness of computer algebra systems, specialisation problem, AISC topics, Integration of logical reasoning and computer algebra, Computer algebra, coding theory, automated theorem provers
25	B. Kutzler	Careful Algebraic Translations of Geometry Theorems.	ISSAC	1989	DBLP DOI BibTeX RDF	computational analytical geometry, automated geometry theorem proving
25	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
25	Eric A. Brewer	A certain freedom: thoughts on the CAP theorem.	PODC	2010	DBLP DOI BibTeX RDF	cap theorem
25	Jie Zhou, Yong-hao Ou	Key Tree and Chinese Remainder Theorem Based Group Key Distribution Scheme.	ICA3PP	2009	DBLP DOI BibTeX RDF	Group Key Distribution Scheme, Key tree, Group member subtree, root ID algorithm, Chinese Remainder Theorem
25	Chung C. Chang, Hsueh-Ming Lu	A Medical Diagnosis Decision Support System Based on Bayesian Theorem and Web Services.	ICA3PP	2009	DBLP DOI BibTeX RDF	Bayesian theorem, web services, SOA, service-oriented architecture, medical decision support systems