Search results for "lemmas"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
128	Fumiaki Okushi, Allen Van Gelder	Persistent and Quasi-Persistent Lemmas in Propositional Model Elimination.	Ann. Math. Artif. Intell.	2004	DBLP DOI BibTeX RDF	Modoc, lemmas, satisfiability, resolution, refutation, Model Elimination
89	Deepak Kapur, Mahadevan Subramaniam	Automatic Generation of Simple Lemmas from Recursive Definitions Using Decision Procedures - Preliminary Report.	ASIAN	2003	DBLP DOI BibTeX RDF
69	Larry M. Hines	Hyper-Chaining and Knowledge-Based Theorem Proving.	CADE	1988	DBLP DOI BibTeX RDF
58	Emmanuel Kounalis	Pumping Lemmas for Tree Languages Generated by Rewrite Systems.	MFCS	1990	DBLP DOI BibTeX RDF	Ground normal forms, Finiteness, Language representation, Compiling pattern-matching, Rewrite systems, Equations, Learning from examples, Finite models, Pumping Lemmas, Negation as failure, Proof by induction, Context-sensitive languages
55	Emanuele Viola, Avi Wigderson	Norms, XOR Lemmas, and Lower Bounds for GF(2) Polynomials and Multiparty Protocols.	CCC	2007	DBLP DOI BibTeX RDF
55	Katia Folegati, Roberto Segala	Coin Lemmas with Random Variables.	PAPM-PROBMIV	2001	DBLP DOI BibTeX RDF
50	Magnus Björk	First Order Stålmarck.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Stålmarck’s method, Universal lemmas, First order logic, Automated theorem proving, Intersections
46	Karen Zee, Viktor Kuncak, Martin C. Rinard	An integrated proof language for imperative programs.	PLDI	2009	DBLP DOI BibTeX RDF	verification, theorem prover, proof system
46	Kamal Aboul-Hosn, Terese Andersen	A Proof-Theoretic Approach to Hierarchical Math Library Organization.	MKM	2005	DBLP DOI BibTeX RDF
46	Jens Schönherr, Bernd Straube	Automatic Equivalence Check of Circuit Descriptions at Clocked Algorithmic and Register Transfer Level.	DATE	2000	DBLP DOI BibTeX RDF
43	Huu Hai Nguyen, Wei-Ngan Chin	Enhancing Program Verification with Lemmas.	CAV	2008	DBLP DOI BibTeX RDF	Lemma Proving, Lemma Application, Program Verification, Separation Logic, Entailment
43	Javier Herranz, Germán Sáez	Forking Lemmas for Ring Signature Schemes.	INDOCRYPT	2003	DBLP DOI BibTeX RDF
35	Ruben A. Gamboa	A Formalization of Powerlist Algebra in ACL2.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Powerlists, Verification, ACL2
35	Brendan Nagle, Annika Poerschke, Vojtech Rödl, Mathias Schacht	Hypergraph regularity and quasi-randomness.	SODA	2009	DBLP DOI BibTeX RDF
35	Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani	A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories.	SAT	2007	DBLP DOI BibTeX RDF
35	Andre Renaud, Padmanabhan Krishnan	An Environment for Specifying and Verifying Security Properties.	Australian Software Engineering Conference	2001	DBLP DOI BibTeX RDF
35	Catherine Meadows 0001	Language generation and verification in the NRL protocol analyzer.	CSFW	1996	DBLP DOI BibTeX RDF	language verification, NRL protocol analyzer, infinite classes of states, cryptography, formal verification, cryptographic protocols, formal languages, formal languages, access protocols, security properties, exhaustive search, language generation
35	Deepak Kapur, Mahadevan Subramaniam	Lemma Discovery in Automated Induction.	CADE	1996	DBLP DOI BibTeX RDF
35	Geoff Sutcliffe	A Comparison of Mechanisms for Avoiding Repetition of Subdeductions in Chain Formal Linear Deduction Systems.	LPAR	1993	DBLP DOI BibTeX RDF
35	Dave Barker-Plummer, Alex Rothenberg	The GAZER Theorem Prover.	CADE	1992	DBLP DOI BibTeX RDF
32	Chuzo Iwamoto, Naoki Hatayama, Yoshiaki Nakashiba, Kenichi Morita, Katsunobu Imai	Translational lemmas for DLOGTIME-uniform circuits, alternating TMs, and PRAMs.	Acta Informatica	2007	DBLP DOI BibTeX RDF
32	Guido Gherardi	An Analysis of the Lemmas of Urysohn and Urysohn-Tietze According to Effective Borel Measurability.	CiE	2006	DBLP DOI BibTeX RDF	Borel Measurability, Urysohn Lemma, Urysohn-Tietze Lemma, Computable Analysis
32	Chuzo Iwamoto, Yoshiaki Nakashiba, Kenichi Morita, Katsunobu Imai	Translational Lemmas for Alternating TMs and PRAMs.	FCT	2005	DBLP DOI BibTeX RDF
32	Yair Bartal	Graph Decomposition Lemmas and Their Role in Metric Embedding Methods.	ESA	2004	DBLP DOI BibTeX RDF
32	Deepak Kapur, Nikita A. Sakhanenko	Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions.	TPHOLs	2003	DBLP DOI BibTeX RDF
32	Ryuzo Hasegawa, Hiroshi Fujita 0002, Miyuki Koshimura	Efficient Minimal Model Generation Using Branching Lemmas.	CADE	2000	DBLP DOI BibTeX RDF
27	Florentina Tone	On the Long-Time H 2-Stability of the Implicit Euler Scheme for the 2D Magnetohydrodynamics Equations.	J. Sci. Comput.	2009	DBLP DOI BibTeX RDF	Magnetohydrodynamics equations, Discrete Gronwall lemmas, Implicit Euler scheme
27	Paul Beame, Russell Impagliazzo, Toniann Pitassi	Improved Depth Lower Bounds for Small Distance Connectivity.	Comput. Complex.	1998	DBLP DOI BibTeX RDF	switching lemmas, resource tradeoffs, Circuit complexity, graph connectivity
27	Michael E. Saks, Aravind Srinivasan, Shiyu Zhou	Explicit OR-Dispersers with Polylogarithmic Degree.	J. ACM	1998	DBLP DOI BibTeX RDF	hashing lemmas, imperfect sources of randomness, measures of information, hardness of approximation, derandomization, expander graphs, time-space tradeoffs, pseudo-random generators, explicit constructions, randomized computation
27	Michael G. Main, Walter Bucher, David Haussler	Applications of an Infinite Squarefree CO-CFL.	ICALP	1985	DBLP DOI BibTeX RDF	syntactic monoids, locally linear languages, Context-free languages, repetitions, pumping lemmas
23	Xiangxue Jia, Runming Lu, Sheng Liu, Jian Zhang 0001	Local lemma: a new strategy of pruning in SAT solvers.	SAC	2010	DBLP DOI BibTeX RDF
23	Adam Chlipala	A verified compiler for an impure functional language.	POPL	2010	DBLP DOI BibTeX RDF	compiler verification, interactive proof assistants
23	Ya-li Peng, Yang Li, Zhang Liang, Xia-ling Zeng, Min Yu	The Research of MovementControl Policy on Tiered Mobile Network.	ICNSC	2008	DBLP DOI BibTeX RDF
23	Jiun-Long Huang, Ming-Syan Chen	A QoS-Aware and Energy-Conserving Transcoding Proxy Using On-Demand Data Broadcasting.	IEEE Trans. Mob. Comput.	2007	DBLP DOI BibTeX RDF	QoS, energy-conservation, data broadcast, on-demand broadcast, Transcoding proxy
23	Reynald Affeldt, Miki Tanaka, Nicolas Marti	Formal Proof of Provable Security by Game-Playing in a Proof Assistant.	ProvSec	2007	DBLP DOI BibTeX RDF
23	Dale Miller 0001, Vivek Nigam	Incorporating Tables into Proofs.	CSL	2007	DBLP DOI BibTeX RDF
23	Xiaofeng Yuan, Hualong Xu, Shuhong Chen	Improvement on the Constrained Association Rule Mining Algorithm of Separate.	ICDIM	2006	DBLP DOI BibTeX RDF
23	Jianmin Pang, Paul Callaghan, Zhaohui Luo	LFTOP: An LF-Based Approach to Domain-Specific Reasoning.	J. Comput. Sci. Technol.	2005	DBLP DOI BibTeX RDF	type theory, logical framework, proof assistant, domain-specific, formal reasoning
23	Penny E. Haxell, Brendan Nagle, Vojtech Rödl	An Algorithmic Version of the Hypergraph Regularity Method.	FOCS	2005	DBLP DOI BibTeX RDF
23	Amy P. Felty	A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code.	RTA	2005	DBLP DOI BibTeX RDF
23	Benoît Sagot	Automatic Acquisition of a Slovak Lexicon from a Raw Corpus.	TSD	2005	DBLP DOI BibTeX RDF
23	Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr	Cut-Elimination: Experiments with CERES.	LPAR	2004	DBLP DOI BibTeX RDF
23	John V. Franco, Michal Kouril, John S. Schlipf, Jeffrey Ward, Sean A. Weaver, Michael R. Dransfield, W. Mark Vanfleet	SBSAT: a State-Based, BDD-Based Satisfiability Solver.	SAT	2003	DBLP DOI BibTeX RDF
23	Reinhold Letz, Gernot Stenz	Universal Variables in Disconnection Tableaux.	TABLEAUX	2003	DBLP DOI BibTeX RDF
23	Yoshiharu Kohayakawa, Brendan Nagle, Vojtech Rödl	Efficient Testing of Hypergraphs.	ICALP	2002	DBLP DOI BibTeX RDF
23	Reinhold Letz	Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas.	TABLEAUX	2002	DBLP DOI BibTeX RDF
23	Andrew W. Appel, Amy P. Felty	A Semantic Model of Types and Machine Instructions for Proof-Carrying Code.	POPL	2000	DBLP DOI BibTeX RDF
23	Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani	Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems.	CAV	1999	DBLP DOI BibTeX RDF
23	Paulo Fernandes 0001, Brigitte Plateau, William J. Stewart 0001	Efficient Descriptor-Vector Multiplications in Stochastic Automata Networks.	J. ACM	1998	DBLP DOI BibTeX RDF	generalized tensor algebra, vector-descriptor multiplication, Markov chains, stochastic automata networks
23	David Taniar	Forward vs. Reverse Traversal in Path Expression Query Processing.	TOOLS (28)	1998	DBLP DOI BibTeX RDF	Forward Traversals, Reverse Traversals, Object-Oriented Query Processing, Path Expression Queries and Performance Evaluation
23	Maria Paola Bonacina, Jieh Hsiang	On Semantic Resolution with Lemmaizing and Contraction.	PRICAI	1996	DBLP DOI BibTeX RDF
23	Roberto Di Cosmo	On the Power of Simple Diagrams.	RTA	1996	DBLP DOI BibTeX RDF
23	Cristina Cornes, Delphine Terrasse	Automating Inversion of Inductive Predicates in Coq.	TYPES	1995	DBLP DOI BibTeX RDF
23	François Bronsard, Uday S. Reddy, Robert W. Hasker	Induction using Term Orderings.	CADE	1994	DBLP DOI BibTeX RDF
23	Frank Pfenning, Dan Nesmith	Presenting Intuitive Deductions via Symmetric Simplification.	CADE	1990	DBLP DOI BibTeX RDF
23	Paul Y. Gloess	An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions.	CADE	1980	DBLP DOI BibTeX RDF
23	Barry K. Rosen	Monoids for Rapid Data Flow Analysis.	POPL	1978	DBLP DOI BibTeX RDF
20	Jia-Rui Zhang, Jun-Guo Lu	Positive Real Lemmas for Fractional-Order Two-Dimensional Roesser Model: The $0< \rho _1\le 1,0<\rho _2\le 1$ Case.	Circuits Syst. Signal Process.	2024	DBLP DOI BibTeX RDF
20	Eric Blais, Cameron Seth	New Graph and Hypergraph Container Lemmas with Applications in Property Testing.	CoRR	2024	DBLP DOI BibTeX RDF
20	Alfredo Hubard, Hugo Parlier	Crossing lemmas for k-systems of arcs.	CoRR	2024	DBLP DOI BibTeX RDF
20	Xianhe Meng, Xian Zhang 0002, Yantao Wang	Bounded real lemmas and exponential H∞ control for memristor-based neural networks with unbounded time-varying delays.	Math. Comput. Simul.	2023	DBLP DOI BibTeX RDF
20	Fang Liu 0014, Haitao Liu, Yong Li 0016, Denis N. Sidorov	Two relaxed quadratic function negative-determination lemmas: Application to time-delay systems.	Autom.	2023	DBLP DOI BibTeX RDF
20	Fanchao Kong, Quanxin Zhu, Cheng Hu 0005, Tingwen Huang	New Inequality Approaches for Fixed-Time Stability Lemmas and Application to Discontinuous CGNNs With Nondifferentiable Delays.	IEEE Trans. Syst. Man Cybern. Syst.	2023	DBLP DOI BibTeX RDF
20	Siddharth Iyer, Anup Rao 0001	XOR Lemmas for Communication via Marginal Information.	Electron. Colloquium Comput. Complex.	2023	DBLP BibTeX RDF
20	Michael Rawson 0001, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel	Lemmas: Generation, Selection, Application.	CoRR	2023	DBLP DOI BibTeX RDF
20	Zhiyong Sun	A gathering of Barbalat's lemmas and their (unsung) cousins.	CoRR	2023	DBLP DOI BibTeX RDF
20	Guorong Gao, Jie Ma, Mingyuan Rong, Tuan Tran	Complexity of null dynamical systems and Sauer-Shelah lemmas.	CoRR	2023	DBLP DOI BibTeX RDF
20	Siddharth Iyer, Anup Rao 0001	XOR Lemmas for Communication via Marginal Information.	CoRR	2023	DBLP DOI BibTeX RDF
20	Greg Bodwin, Lily Wang	Improved Shortest Path Restoration Lemmas for Multiple Edge Failures: Trade-offs Between Fault-tolerance and Subpaths.	CoRR	2023	DBLP DOI BibTeX RDF
20	Michael P. Casey	Bulk Johnson-Lindenstrauss Lemmas.	CoRR	2023	DBLP DOI BibTeX RDF
20	Rindo Nakanishi, Yoshiaki Takata, Hiroyuki Seki	Pumping Lemmas for Languages Expressed by Computational Models with Registers.	IEICE Trans. Inf. Syst.	2023	DBLP DOI BibTeX RDF
20	Xian Zhang 0002, Xianhe Meng, Yantao Wang, Chunyan Liu	Bounded real lemmas for inertial neural networks with unbounded mixed delays and state-dependent switching.	Commun. Nonlinear Sci. Numer. Simul.	2023	DBLP DOI BibTeX RDF
20	Olivier Danvy	Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant - ERRATUM.	J. Funct. Program.	2023	DBLP DOI BibTeX RDF
20	Fanchao Kong, Quanxin Zhu	Fixed-Time Stabilization of Discontinuous Neutral Neural Networks With Proportional Delays via New Fixed-Time Stability Lemmas.	IEEE Trans. Neural Networks Learn. Syst.	2023	DBLP DOI BibTeX RDF
20	Yechuan Xia, Anna Becchi, Alessandro Cimatti, Alberto Griggio, Jianwen Li, Geguang Pu	Searching for i-Good Lemmas to Accelerate Safety Model Checking.	CAV (2)	2023	DBLP DOI BibTeX RDF
20	Michael Rawson 0001, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel	Lemmas: Generation, Selection, Application.	TABLEAUX	2023	DBLP DOI BibTeX RDF
20	Adithya Murali, Lucas Peña, Eion Blanchard, Christof Löding, P. Madhusudan	Model-guided synthesis of inductive lemmas for FOL with least fixpoints.	Proc. ACM Program. Lang.	2022	DBLP DOI BibTeX RDF
20	Matteo Pellegrini, Marco Passarotti, Eleonora Litta, Francesco Mambrini, Giovanni Moretti, Claudia Corbetta, Martina Verdelli	Enhancing Derivational Information on Latin Lemmas in the LiLa Knowledge Base. A Structural and Diachronic Extension.	Prague Bull. Math. Linguistics	2022	DBLP BibTeX RDF
20	Jacob Fox, Yufei Zhao	Removal lemmas and approximate homomorphisms.	Comb. Probab. Comput.	2022	DBLP DOI BibTeX RDF
20	Rocco A. Servedio, Li-Yang Tan	Improved Pseudorandom Generators from Pseudorandom Multi-switching Lemmas.	Theory Comput.	2022	DBLP BibTeX RDF
20	Jürgen Dassow, Ismaël Jecker	Operational complexity and pumping lemmas.	Acta Informatica	2022	DBLP DOI BibTeX RDF
20	Neil Thapen	Notes on switching lemmas.	CoRR	2022	DBLP BibTeX RDF
20	Yiyang Huang, Clément L. Canonne	Lemmas of Differential Privacy.	CoRR	2022	DBLP DOI BibTeX RDF
20	Uriya A. First, Tali Kaufman	Couboundary Expansion of Sheaves on Graphs and Weighted Mixing Lemmas.	CoRR	2022	DBLP DOI BibTeX RDF
20	Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar	Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs.	J. Autom. Reason.	2022	DBLP DOI BibTeX RDF
20	Véronique Cortier, Stéphanie Delaune, Jannik Dreier, Elise Klein 0002	Automatic generation of sources lemmas in Tamarin: Towards automatic proofs of security protocols.	J. Comput. Secur.	2022	DBLP DOI BibTeX RDF
20	Olivier Danvy	Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant.	J. Funct. Program.	2022	DBLP DOI BibTeX RDF
20	Kazuko Takahashi	Odd or Even: Handling N-lemmas in a Dynamic Argumentation Framework.	SAFA@COMMA	2022	DBLP BibTeX RDF
20	Bruno Blanchet, Vincent Cheval, Véronique Cortier	ProVerif with Lemmas, Induction, Fast Subsumption, and Much More.	SP	2022	DBLP DOI BibTeX RDF
20	Noga Alon, Guy Moshkovitz	Limitations on regularity lemmas for clustering graphs.	Adv. Appl. Math.	2021	DBLP DOI BibTeX RDF
20	Fan Chung	Regularity lemmas for clustering graphs.	Adv. Appl. Math.	2021	DBLP DOI BibTeX RDF
20	Qing-Hao Zhang, Jun-Guo Lu	Bounded Real Lemmas for Singular Fractional-Order Systems: The 1 < α < 2 Case.	IEEE Trans. Circuits Syst. II Express Briefs	2021	DBLP DOI BibTeX RDF
20	Bhavana R. Bhamare, Jeyanthi Prabhu	A supervised scheme for aspect extraction in sentiment analysis using the hybrid feature set of word dependency relations and lemmas.	PeerJ Comput. Sci.	2021	DBLP DOI BibTeX RDF
20	Owen Biesel	A Principle for Converting Lindström-Type Lemmas to Stembridge-Type Theorems, with Applications to Walks, Groves, and Alternating Flows.	Graphs Comb.	2021	DBLP DOI BibTeX RDF
20	Liang Ma 0002, Ting He 0001, Kin K. Leung, Don Towsley, Ananthram Swami	Additive Link Metrics Identification: Proof of Selected Lemmas and Propositions.	CoRR	2021	DBLP BibTeX RDF
20	Bruce Changlong Xu	Separating Circuits : Switching Lemmas and Random Restrictions.	CoRR	2021	DBLP BibTeX RDF
20	Tomoyuki Yamakami	Intersection and Union Hierarchies of Deterministic Context-Free Languages and Pumping Lemmas.	CoRR	2021	DBLP BibTeX RDF
20	Agnishom Chattopadhyay, Filip Mazowiecki, Anca Muscholl, Cristian Riveros	Pumping lemmas for weighted automata.	Log. Methods Comput. Sci.	2021	DBLP DOI BibTeX RDF
20	Rob Arthan, Paulo Oliva	On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem.	J. Log. Anal.	2021	DBLP BibTeX RDF
20	Fanchao Kong, Quanxin Zhu, Tingwen Huang	New Fixed-Time Stability Lemmas and Applications to the Discontinuous Fuzzy Inertial Neural Networks.	IEEE Trans. Fuzzy Syst.	2021	DBLP DOI BibTeX RDF