Tag #theorem
261 papers:
CSL-2020-Passmann #set- De Jongh's Theorem for Intuitionistic Zermelo-Fraenkel Set Theory (RP), p. 16.
- ICFP-2019-0001A #compilation #correctness #functional
- The next 700 compiler correctness theorems (functional pearl) (DP0, AA), p. 29.
ICML-2019-Dohmatob #robust- Generalized No Free Lunch Theorem for Adversarial Robustness (ED), pp. 1646–1654.
- ICML-2019-YangD #learning #proving
- Learning to Prove Theorems via Interacting with Proof Assistants (KY, JD), pp. 6984–6994.
POPL-2019-GorogiannisOS #detection- A true positives theorem for a static race detector (NG, PWO, IS), p. 29.
CADE-2019-0001T - A Formally Verified Abstract Account of Gödel's Incompleteness Theorems (AP0, DT), pp. 442–461.
DLT-2018-CartonP #word- Simon's Theorem for Scattered Words (OC, MP), pp. 182–193.
- DLT-2018-I
- The Runs Theorem and Beyond (TI), pp. 18–23.
- CSL-2018-AlcoleiCHW #concurrent
- The True Concurrency of Herbrand's Theorem (AA, PC, MH, GW), p. 22.
FSCD-2017-Silva #concurrent- Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages (Invited Talk) (AS0), p. 1.
- ICFP-2017-AhmedJSW #for free #parametricity
- Theorems for free for free: parametricity, with and without types (AA, DJ, JGS, PW), p. 28.
CIG-2017-AshlockPS #game studies #video- General video game playing escapes the no free lunch theorem (DA, DPL, AS), pp. 17–24.
- POPL-2017-SrikanthSH #complexity #using #verification
- Complexity verification using guided theorem enumeration (AS, BS, WRH), pp. 639–652.
CASE-2017-LiuH17a #analysis #cyber-physical #hybrid- Hybrid stability analysis via extended small-gain theorem for networked cyber-physical systems with transmission delay (QL, QH), pp. 1598–1603.
- ICML-2016-FriesenD #learning #modelling
- The Sum-Product Theorem: A Foundation for Learning Tractable Models (ALF, PMD), pp. 1909–1918.
- CSL-2016-FavoniaS #type system
- The Seifert-van Kampen Theorem in Homotopy Type Theory (KBH(, MS), p. 16.
- CSL-2016-KolodziejczykMP #automaton #decidability #logic
- The Logical Strength of Büchi's Decidability Theorem (LAK, HM, PP, MS), p. 16.
IJCAR-2016-DawsonBG #calculus #logic #using- Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi (JED, JB, RG), pp. 452–468.
TAP-2016-Liu #specification #testing #verification- Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification (SL), pp. 112–129.
VMCAI-2016-MarechalFKMP #approximate #multi #using- Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem (AM, AF, TK0, DM, MP), pp. 166–184.
ICALP-v2-2015-Finkel #automaton #infinity #scalability #word- Incompleteness Theorems, Large Cardinals, and Automata over Infinite Words (OF), pp. 222–233.
- ICALP-v2-2015-KawarabayashiK #graph #towards
- Towards the Graph Minor Theorems for Directed Graphs (KiK, SK), pp. 3–10.
LATA-2015-BabariD #automaton #logic- A Nivat Theorem for Weighted Picture Automata and Weighted MSO Logic (PB, MD), pp. 703–715.
- LATA-2015-LuckMS #complexity
- Parameterized Complexity of CTL — A Generalization of Courcelle’s Theorem (ML, AM, IS), pp. 549–560.
- ICML-2015-KairouzOV #composition #difference #privacy
- The Composition Theorem for Differential Privacy (PK, SO, PV), pp. 1376–1385.
STOC-2015-Barman #approximate #nash- Approximating Nash Equilibria and Dense Bipartite Subgraphs via an Approximate Version of Caratheodory’s Theorem (SB), pp. 361–369.
- STOC-2015-Chuzhoy #grid
- Excluded Grid Theorem: Improved and Simplified (JC), pp. 645–654.
- STOC-2015-KawarabayashiK #grid
- The Directed Grid Theorem (KiK, SK), pp. 655–664.
- CSL-2015-KontinenMSV #semantics
- A Van Benthem Theorem for Modal Team Semantics (JK, JSM, HS, HV), pp. 277–291.
- DLT-J-2013-DrosteV14 #context-free grammar
- The Chomsky-SCHüTzenberger Theorem for Quantitative Context-Free Languages (MD, HV), pp. 955–970.
- DLT-2014-KarhumakiSZ #equivalence
- Variations of the Morse-Hedlund Theorem for k-Abelian Equivalence (JK, AS, LQZ), pp. 203–214.
- ICALP-v2-2014-DrosteP #automaton #distance #logic
- A Nivat Theorem for Weighted Timed Automata and Weighted Relative Distance Logic (MD, VP), pp. 171–182.
RTA-TLCA-2014-BerardiS - Ramsey Theorem as an Intuitionistic Property of Well Founded Relations (SB, SS), pp. 93–107.
- ICML-c2-2014-ArgyriouD
- A Unifying View of Representer Theorems (AA, FD), pp. 748–756.
- POPL-2014-AccattoliBKL #standard
- A nonstandard standardization theorem (BA, EB, DK, CL), pp. 659–670.
- POPL-2014-Atkey #parametricity
- From parametricity to conservation laws, via Noether’s theorem (RA), pp. 491–502.
PPDP-2014-AotoS #induction #proving- Decision Procedures for Proving Inductive Theorems without Induction (TA, SS), pp. 237–248.
- PPDP-2014-MehnerSSV #functional #parametricity #proving
- Parametricity and Proving Free Theorems for Functional-Logic Languages (SM, DS, LS, JV), pp. 19–30.
FoSSaCS-2014-AdamekMMU - Generalized Eilenberg Theorem I: Local Varieties of Languages (JA, SM, RSRM, HU), pp. 366–380.
- STOC-2014-ChekuriC #bound #polynomial
- Polynomial bounds for the grid-minor theorem (CC, JC), pp. 60–69.
- STOC-2014-KawarabayashiKK #graph #grid #problem
- An excluded half-integral grid theorem for digraphs and the directed disjoint paths problem (KiK, YK, SK), pp. 70–78.
- STOC-2014-Yoshida #composition #invariant
- A characterization of locally testable affine-invariant properties via decomposition theorems (YY), pp. 154–163.
LICS-CSL-2014-BojanczykDK #calculus #composition #model checking #μ-calculus- Decomposition theorems and model-checking for the modal μ-calculus (MB, CD, SK), p. 10.
- LICS-CSL-2014-HarwathHS #bound #composition
- Preservation and decomposition theorems for bounded degree structures (FH, LH, NS), p. 10.
- LICS-CSL-2014-Mahboubi #order #proving
- Computer-checked mathematics: a formal proof of the odd order theorem (AM), p. 1.
SAT-2014-IstrateC #complexity #proving- Proof Complexity and the Kneser-Lovász Theorem (GI, AC), pp. 138–153.
- DLT-J-2012-KarhumakiPS13
- Fine and Wilf’s Theorem for k-Abelian Periods (JK, SP, AS), pp. 1135–1152.
CIAA-2013-ChistikovM #word- A Uniformization Theorem for Nested Word to Word Transductions (DVC, RM), pp. 97–108.
- DLT-2013-DrosteV #context-free grammar
- The Chomsky-Schützenberger Theorem for Quantitative Context-Free Languages (MD, HV), pp. 203–214.
- ICALP-v1-2013-ODonnellT #composition #fourier
- A Composition Theorem for the Fourier Entropy-Influence Conjecture (RO, LYT), pp. 780–791.
- ICALP-v2-2013-BartheO #composition #difference #logic #privacy #probability #relational #source code
- Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs (GB, FO), pp. 49–60.
TLCA-2013-KrausECA - Generalizations of Hedberg’s Theorem (NK, MHE, TC, TA), pp. 173–188.
ICFP-2013-Morihata #parallel- A short cut to parallelization theorems (AM), pp. 245–256.
- ICML-c1-2013-YuCSS
- Characterizing the Representer Theorem (YY, HC, DS, CS), pp. 570–578.
LOPSTR-2013-AransayD #algebra #algorithm #execution #formal method #linear- Formalization and Execution of Linear Algebra: From Theorems to Algorithms (JA, JD), pp. 1–18.
- POPL-2013-Gonthier #order #proving
- Engineering mathematics: the odd order theorem proof (GG), pp. 1–2.
- STOC-2013-BrandaoH #metric #quantum
- Quantum de finetti theorems under local measurements with applications (FGSLB, AWH), pp. 861–870.
- STOC-2013-LeeMM
- A node-capacitated okamura-seymour theorem (JRL, MM, MM), pp. 495–504.
- STOC-2013-SinclairS #complexity
- Lee-Yang theorems and the complexity of computing averages (AS, PS), pp. 625–634.
- LICS-2013-FacchiniVZ #calculus #μ-calculus
- A Characterization Theorem for the Alternation-Free Fragment of the Modal μ-Calculus (AF, YV, FZ), pp. 478–487.
- SAT-2013-Lauria #bound #proving #rank
- A Rank Lower Bound for Cutting Planes Proofs of Ramsey’s Theorem (ML), pp. 351–364.
- DLT-2012-KapoutsisL #automaton #finite #nondeterminism
- Analogs of Fagin’s Theorem for Small Nondeterministic Finite Automata (CAK, NL), pp. 202–213.
- DLT-2012-KarhumakiPS
- Fine and Wilf’s Theorem for k-Abelian Periods (JK, SP, AS), pp. 296–307.
- DLT-2012-Okhotin
- Non-erasing Variants of the Chomsky-Schützenberger Theorem (AO), pp. 121–129.
- RTA-2012-Accattoli
- An Abstract Factorization Theorem for Explicit Substitutions (BA), pp. 6–21.
- STOC-2012-GroheM #graph #morphism
- Structure theorem and isomorphism test for graphs with excluded topological subgraphs (MG, DM), pp. 173–192.
- STOC-2012-MosselR
- A quantitative gibbard-satterthwaite theorem without neutrality (EM, MZR), pp. 1041–1060.
- CSL-2012-Rabinovich #proving
- A Proof of Kamp’s theorem (AR), pp. 516–527.
ICLP-J-2012-BabbL #modelling- Module theorem for the general theory of stable models (JB, JL), pp. 719–735.
- LICS-2012-ChenM #algebra #category theory #constraints #quantifier
- An Algebraic Preservation Theorem for Aleph-Zero Categorical Quantified Constraint Satisfaction (HC, MM), pp. 215–224.
- DLT-J-2009-BrzozowskiGS11 #formal method
- Closures in Formal Languages and Kuratowski’s Theorem (JAB, EG, JS), pp. 301–321.
- DLT-J-2009-GazdagN11
- A Kleene Theorem for Bisemigroup and binoid Languages (ZG, ZLN), pp. 427–446.
- DLT-2011-Shallit #revisited
- Fife’s Theorem Revisited (JS), pp. 397–405.
- ICALP-v2-2011-Delacourt #automaton #set
- Rice’s Theorem for μ-Limit Sets of Cellular Automata (MD), pp. 89–100.
- RTA-2011-AotoYC #higher-order #induction
- Natural Inductive Theorems for Higher-Order Rewriting (TA, TY, YC), pp. 107–121.
- TLCA-2011-ManzonettoP #λ-calculus
- Böhm’s Theorem for Resource λ Calculus through Taylor Expansion (GM, MP), pp. 153–168.
- ICFP-2011-MuM #functional #morphism
- Generalising and dualising the third list-homomorphism theorem: functional pearl (SCM, AM), pp. 385–391.
OOPSLA-2011-DelawareCB #product line- Product lines of theorems (BD, WRC, DSB), pp. 595–608.
- STOC-2011-BodirskyP #graph
- Schaefer’s theorem for graphs (MB, MP), pp. 655–664.
- STOC-2011-Sherstov #communication #complexity #quantum #query
- Strong direct product theorems for quantum communication and query complexity (AAS), pp. 41–50.
AFL-J-2008-Blanchet-SadriOR10 #word- Fine and Wilf’s Theorem for Partial Words with Arbitrarily Many Weak Periods (FBS, TO, TDR), pp. 705–722.
- CIAA-2010-Grosu #commutative
- The Cayley-Hamilton Theorem for Noncommutative Semirings (RG), pp. 143–153.
- DLT-2010-DrosteV #automaton #bound #logic #multi
- Kleene and Büchi Theorems for Weighted Automata and Multi-valued Logics over Arbitrary Bounded Lattices (MD, HV), pp. 160–172.
- ICALP-v1-2010-CaiCL #graph #morphism
- Graph Homomorphisms with Complex Values: A Dichotomy Theorem (JyC, XC, PL), pp. 275–286.
- ICALP-v1-2010-LeeZ #communication #complexity #composition
- Composition Theorems in Communication Complexity (TL, SZ), pp. 475–489.
- ICALP-v1-2010-Xia #artificial reality #reduction
- Holographic Reduction: A Domain Changed Application and Its Partial Converse Theorems (MX), pp. 666–677.
FLOPS-2010-SeidelV #automation #generative- Automatically Generating Counterexamples to Naive Free Theorems (DS, JV), pp. 175–190.
ICPR-2010-DursunDG #2d #image #re-engineering #slicing- Paired Transform Slice Theorem of 2-D Image Reconstruction from Projections (SD, ND, AMG), pp. 2395–2398.
- STOC-2010-KawarabayashiW #algorithm #graph #proving
- A shorter proof of the graph minor algorithm: the unique linkage theorem (KiK, PW), pp. 687–694.
- STOC-2010-Klauck
- A strong direct product theorem for disjointness (HK), pp. 77–86.
SIGMOD-2009-Kifer #privacy- Attacks on privacy and deFinetti’s theorem (DK), pp. 127–138.
- DLT-2009-BrzozowskiGS #formal method
- Closures in Formal Languages and Kuratowski’s Theorem (JAB, EG, JS), pp. 125–144.
- DLT-2009-Saarela #complexity #equation #on the #satisfiability
- On the Complexity of Hmelevskii’s Theorem and Satisfiability of Three Unknown Equations (AS), pp. 443–453.
- ICALP-v1-2009-GuhaH #bound #order #random
- Revisiting the Direct Sum Theorem and Space Lower Bounds in Random Order Streams (SG, ZH), pp. 513–524.
- ICALP-v2-2009-DaskalakisP #network #on the
- On a Network Generalization of the Minmax Theorem (CD, CHP), pp. 423–434.
- LATA-2009-Strassburger
- A Kleene Theorem for Forest Languages (LS), pp. 715–727.
- TLCA-2009-Pagani #difference
- The Cut-Elimination Theorem for Differential Nets with Promotion (MP), pp. 219–233.
- ICFP-2009-Voigtlander #functional
- Free theorems involving type constructor classes: functional pearl (JV), pp. 173–184.
- POPL-2009-MorihataMHT #divide and conquer #morphism
- The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer (AM, KM, ZH, MT), pp. 177–185.
SAC-2009-MagaudNS #coq #formal method #using- Formalizing Desargues’ theorem in Coq using ranks (NM, JN, PS), pp. 1110–1115.
- FoSSaCS-2009-BonsangueRS #algebra #polynomial
- A Kleene Theorem for Polynomial Coalgebras (MMB, JJMMR, AS), pp. 122–136.
- CADE-2009-BoigelotBL #automaton
- A Generalization of Semenov’s Theorem to Automata over Real Numbers (BB, JB, JL), pp. 469–484.
- CSL-2009-Moschovakis #recursion
- Kleene’s Amazing Second Recursion Theorem (YNM), pp. 24–39.
- AFL-2008-GazdagN
- A Kleene Theorem for Binoid Languages (ZG, ZLN), pp. 170–182.
- DLT-2008-KarhumakiS #analysis
- An Analysis and a Reproof of Hmelevskii’s Theorem (JK, AS), pp. 467–478.
- ICALP-A-2008-LeeM #programming
- Product Theorems Via Semidefinite Programming (TL, RM), pp. 674–685.
- ICALP-B-2008-YokoyamaAG
- Reversible Flowchart Languages and the Structured Reversible Program Theorem (TY, HBA, RG), pp. 258–270.
- LATA-2008-Steinberg #matrix #sequence
- Subsequence Counting, Matrix Representations and a Theorem of Eilenberg (BS), pp. 6–10.
IFL-2008-Hinze #proving- Scans and Convolutions — A Calculational Proof of Moessner’s Theorem (RH), pp. 1–24.
BX-2008-Voigtlaender1 #bidirectional- Free Theorems and Bidirectional Transformations (JV), p. 30.
PEPM-2008-Voigtlander #correctness #proving- Proving correctness via free theorems: the case of the destroy/build-rule (JV), pp. 13–20.
- POPL-2008-Asperti
- The intensional content of Rice’s theorem (AA), pp. 113–119.
- SAC-2008-Michelucci #geometry #proving #word
- Isometry group, words and proofs of geometric theorems (DM), pp. 1821–1825.
ESOP-2008-MatthewsA #exclamation #morphism #parametricity #polymorphism #runtime- Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices! (JM, AA), pp. 16–31.
- FoSSaCS-2008-DrosteQ #automaton
- A Kleene-Schützenberger Theorem for Weighted Timed Automata (MD, KQ), pp. 142–156.
- STOC-2008-BorgsCIKMP
- The myth of the folk theorem (CB, JTC, NI, ATK, VSM, CHP), pp. 365–372.
- STOC-2008-ImpagliazzoJKW
- Uniform direct product theorems: simplified, optimized, and derandomized (RI, RJ, VK, AW), pp. 579–588.
- STOC-2008-JainKN #bound #communication #complexity
- Direct product theorems for classical communication complexity via subdistribution bounds: extended abstract (RJ, HK, AN), pp. 599–608.
- STOC-2008-Nandakumar #effectiveness
- An effective ergodic theorem and some applications (SN), pp. 39–44.
CAV-2008-JoshiK #graph transformation #verification- Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems (SJ, BK), pp. 214–226.
- LICS-2008-Duris
- Hypergraph Acyclicity and Extension Preservation Theorems (DD), pp. 418–427.
- ICALP-2007-BoigelotB #automaton
- A Generalization of Cobham’s Theorem to Automata over Real Numbers (BB, JB), pp. 813–824.
- ICALP-2007-Colcombet #combinator
- A Combinatorial Theorem for Trees (TC), pp. 901–912.
- SAC-2007-Dufourd #framework #proving
- A hypermap framework for computer-aided proofs in surface subdivisions: genus theorem and Euler’s formula (JFD), pp. 757–761.
- STOC-2007-PassV #game studies #parallel #performance
- An efficient parallel repetition theorem for Arthur-Merlin games (RP, MV), pp. 420–429.
- CSL-2007-WeisI #strict #word
- Structure Theorem and Strict Alternation Hierarchy for FO2 on Words (PW, NI), pp. 343–357.
- LICS-2007-CateBV #first-order #logic
- Lindstrom theorems for fragments of first-order logic (BtC, JvB, JAV), pp. 280–292.
- LICS-2007-NguyenC #complexity #proving
- The Complexity of Proving the Discrete Jordan Curve Theorem (PN, SAC), pp. 245–256.
- DLT-J-2005-BesC06 #linear #order #word
- A Kleene Theorem for Languages of Words Indexed by Linear Orderings (AB, OC), pp. 519–542.
- ICPR-v2-2006-HuD #classification #multi
- A “No Panacea Theorem” for Multiple Classifier Combination (RH, RID), pp. 1250–1253.
- ICPR-v3-2006-TanakaFKI
- A Theoretical and Experimental Consideration on Interference in Resolutions between Sampling Theorem and OK-Quantization Theory (YT, TF, HK, TI), pp. 869–872.
- STOC-2006-AmbainisSW #bound #quantum #trade-off
- A new quantum lower bound method, : with applications to direct product theorems and time-space tradeoffs (AA, RS, RdW), pp. 618–633.
- STOC-2006-Dinur
- The PCP theorem by gap amplification (ID), pp. 241–250.
- SAT-2006-ChenIJSS #constraints #problem
- A Dichotomy Theorem for Typed Constraint Satisfaction Problems (SC, TI, KJ, DS, MS), pp. 226–239.
- DLT-2005-BedonR #linear #order #word
- Schützenberger and Eilenberg Theorems for Words on Linear Orderings (NB, CR), pp. 134–145.
- DLT-2005-BesC #linear #order #word
- A Kleene Theorem for Languages of Words Indexed by Linear Orderings (AB, OC), pp. 158–167.
- TLCA-2005-Coquand #λ-calculus
- Completeness Theorems and λ-Calculus (TC), pp. 1–9.
- CSL-2005-Berger #normalisation
- An Abstract Strong Normalization Theorem (UB), pp. 27–35.
- LICS-2005-DawarO
- Modal Characterisation Theorems over Special Classes of Frames (AD, MO), pp. 21–30.
- CIAA-2004-Maletti #transducer
- Myhill-Nerode Theorem for Sequential Transducers over Unique GCD-Monoids (AM), pp. 323–324.
- DLT-2004-GenestMK #algorithm #automaton #communication #effectiveness
- A Kleene Theorem for a Class of Communicating Automata with Effective Algorithms (BG, AM, DK), pp. 30–48.
- ICALP-2004-EdalatP
- A Domain Theoretic Account of Picard’s Theorem (AE, DP), pp. 494–505.
- ICALP-2004-Meer #proving
- Transparent Long Proofs: A First PCP Theorem for NPR (KM), pp. 959–970.
- ICALP-2004-Toftdal #analysis #effectiveness #logic
- A Calibration of Ineffective Theorems of Analysis in a Hierarchy of Semi-classical Logical Principles: (MT), pp. 1188–1200.
- RTA-2004-AotoYT #higher-order #induction
- Inductive Theorems for Higher-Order Rewriting (TA, TY, YT), pp. 269–284.
PLDI-2004-Appel #process #proving #revisited #social #source code- Social processes and proofs of theorems and programs, revisited (AWA), p. 170.
- POPL-2004-JohannV
- Free theorems in the presence of seq (PJ, JV), pp. 99–110.
- STOC-2004-ChenKLRSV #bound #confluence
- (Almost) tight bounds and existence theorems for confluent flows (JC, RDK, LL, RR, RS, AV), pp. 529–538.
- STOC-2004-CorreaG #approximate #graph
- An approximate König’s theorem for edge-coloring weighted bipartite graphs (JRC, MXG), pp. 398–406.
- STOC-2004-Obata #approximate #multi
- Approximate max-integral-flow/min-multicut theorems (KO), pp. 539–545.
- CSL-2004-DawsonG #termination
- A General Theorem on Termination of Rewriting (JED, RG), pp. 100–114.
- IJCAR-2004-ColtonMSM #algebra #automation #classification #finite #generative
- Automatic Generation of Classification Theorems for Finite Algebras (SC, AM, VS, RLM), pp. 400–414.
DRR-2003-CinqueLMR - Fermat theorem and elliptic color histogram features (LC, SL, AM, FDR), pp. 234–240.
- DLT-2003-Borchardt
- The Myhill-Nerode Theorem for Recognizable Tree Series (BB), pp. 146–158.
- ICALP-2003-JainRS #communication #complexity
- A Direct Sum Theorem in Communication Complexity via Message Compression (RJ, JR, PS), pp. 300–315.
- CADE-2003-AvenhausKSW #exclamation #how #induction
- How to Prove Inductive Theorems? QUODLIBET! (JA, UK, TSS, CPW), pp. 328–333.
- CADE-2003-DeplagneKKN #equation #induction #proving
- Proof Search and Proof Check for Equational and Inductive Theorems (ED, CK, HK, QHN), pp. 297–316.
- ICALP-2002-BonichonSM
- Wagner’s Theorem on Realizers (NB, BLS, MM), pp. 1043–1053.
- CADE-2002-Colton #generative
- The HR Program for Theorem Generation (SC), pp. 285–289.
- CADE-2002-Paulson #case study #reasoning
- The Reflection Theorem: A Study in Meta-theoretic Reasoning (LCP), pp. 377–391.
- LICS-2002-Otto #finite
- Modal and Guarded Characterisation Theorems over Finite Transition Systems (MO), p. 371–?.
- CSL-2001-BaazM #on the
- On a Generalisation of Herbrand’s Theorem (MB, GM), pp. 469–483.
- CSL-2001-GalotaV #automaton
- A Generalization of the Büchi-Elgot-Trakhtenbrot Theorem (MG, HV), pp. 355–368.
- CSL-2001-GroheW #locality
- An Existential Locality Theorem (MG, SW), pp. 99–114.
- ICLP-2001-ErdemL #source code
- Fages’ Theorem for Programs with Nested Expressions (EE, VL), pp. 242–254.
- IJCAR-2001-GanzingerM #bottom-up #logic programming #source code
- A New Meta-complexity Theorem for Bottom-Up Logic Programs (HG, DAM), pp. 514–528.
- IJCAR-2001-GieslK #decidability #induction
- Decidable Classes of Inductive Theorems (JG, DK), pp. 469–484.
- LICS-2001-CookK #higher-order #reasoning #using
- A Second-Order System for Polytime Reasoning Using Graedel’s Theorem (SAC, AK), pp. 177–186.
WLC-2000-Shoji #proving- A Proof of Okninski, Putcha’s Theorem (KS), pp. 420–427.
- ICPR-v3-2000-ShenIT00a #2d #image #novel #symmetry
- A Novel Theorem on Symmetries of 2D Images (DS, HHSI, EKT), pp. 7014–7017.
- STOC-2000-Kilian
- More general completeness theorems for secure two-party computation (JK), pp. 316–324.
- LICS-2000-Kripke #algorithm #first-order
- From the Church-Turing Thesis to the First-Order Algorithm Theorem (SK), p. 177.
- LICS-2000-McMillan #model checking #proving
- Some Strategies for Proving Theorems with a Model Checker (KLM), pp. 305–306.
- DLT-1999-KarhumakiM #fault
- Defect theorems for trees (JK, SM), pp. 164–177.
- TLCA-1999-Statman #consistency #equation
- Consequences of Jacopini’s Theorem: Consistent Equalities and Equations (RS), pp. 355–364.
- STOC-1999-CaiNS #probability
- Hardness and Hierarchy Theorems for Probabilistic Quasi-Polynomial Time (JyC, AN, DS), pp. 726–735.
- STOC-1999-GalR
- A Theorem on Sensitivity and Applications in Private Computation (AG, AR), pp. 348–357.
- LICS-1999-HopkinsK #algebra #commutative
- Parikh’s Theorem in Commutative Kleene Algebra (MWH, DK), pp. 394–401.
PODS-1998-SamoladasM #bound #multi #query- A Lower Bound Theorem for Indexing Schemes and Its Application to Multidimensional Range Queries (VS, DPM), pp. 44–51.
- ICALP-1998-Mellies #on the
- On a Duality Between Kruskal and Dershowitz Theorems (PAM), pp. 518–529.
- RTA-1998-Ohlebusch #equivalence #reduction
- Church-Rosser Theorems for Abstract Reduction Modulo an Equivalence Relation (EO), pp. 17–31.
- ALP-PLILP-1998-GoguenMK
- A Hidden Herbrand Theorem (JAG, GM, TK), pp. 445–462.
- STOC-1998-Bshouty #algorithm #composition #learning
- A New Composition Theorem for Learning Algorithms (NHB), pp. 583–589.
- CADE-1998-FeveW #algebra #geometry #proving #using
- Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules (SF, DW), pp. 17–31.
- CSL-1998-Hajek #fuzzy #logic
- Trakhtenbrot Theorem and Fuzzy Logic (PH), pp. 1–8.
- CSL-1998-KomaraV #programming
- Theorems af Péter and Parsons in Computer Programming (JK, PJV), pp. 204–223.
- LICS-1998-Bernstein #congruence #higher-order #semantics
- A Congruence Theorem for Structured Operational Semantics of Higher-Order Languages (KLB), pp. 153–164.
- LICS-1998-Mellies
- A Stability Theorem in Rewriting Theory (PAM), pp. 287–298.
- LICS-1998-Voronkov #automation #reasoning #semantics
- Herbrand’s Theorem, Automated Reasoning and Semantics Tableaux (AV), pp. 252–263.
- ICALP-1997-Roura #divide and conquer
- An Improved Master Theorem for Divide-and-Conquer Recurrences (SR), pp. 449–459.
- STOC-1997-Ben-DavidBK #algorithm #composition #concept #geometry #learning
- A Composition Theorem for Learning Algorithms with Applications to Geometric Concept Classes (SBD, NHB, EK), pp. 324–333.
- LICS-1997-AsarinCM #automaton
- A Kleene Theorem for Timed Automata (EA, PC, OM), pp. 160–171.
- LICS-1997-Janin #automaton #calculus #fixpoint #reduction
- Automata, Tableaus and a Reduction Theorem for Fixpoint Calculi in Arbitrary Complete Lattices (DJ), pp. 172–182.
- ICALP-1996-Lenzi #calculus #μ-calculus
- A Hierarchy Theorem for the μ-Calculus (GL), pp. 87–97.
- RTA-1996-Luth #algebra #composition #proving #term rewriting
- Compositional Term Rewriting: An Algebraic Proof of Toyama’s Theorem (CL), pp. 261–275.
- ICPR-1996-Chernov
- Tauber theorems for Dirichlet series and fractals (VMC), pp. 656–661.
- ICPR-1996-LinF #fourier #re-engineering #slicing #using
- Range data reconstruction using Fourier slice theorem (SSL, CSF), pp. 874–878.
KR-1996-SiegelF #logic #representation- A Representation Theorem for Preferential Logics (PS, LF), pp. 453–460.
- ALP-1996-Suzuki #revisited #standard
- Standardization Theorem Revisited (TS), pp. 122–134.
- CAV-1996-Gribomont #reduction #refinement
- Atomicity Refinement and Trace Reduction Theorems (EPG), pp. 311–322.
- LICS-1996-AbdullaCJT #decidability #infinity
- General Decidability Theorems for Infinite-State Systems (PAA, KC, BJ, YKT), pp. 313–321.
- LICS-1996-MedinaI
- A Generalization of Fagin’s Theorem (JAM, NI), pp. 2–12.
- RTA-1995-Holmes #equation #proving #recursion
- Disguising Recursively Chained Rewrite Rules as Equational Theorems, as Implemented in the Prover EFTTP Mark 2 (MRH), pp. 432–437.
- STOC-1995-GalilY
- Short length versions of Menger’s theorem (ZG, XY), pp. 499–508.
- STOC-1995-Raz #parallel
- A parallel repetition theorem (RR), pp. 447–456.
- ICALP-1994-Droste #concurrent #monad
- A KLeene Theorem for Recognizable Languages over Concurrency Monoids (MD), pp. 388–399.
- ALP-1994-BidoitH #behaviour #first-order #logic #proving #standard
- Proving Behavioural Theorems with Standard First-Order Logic (MB, RH), pp. 41–58.
- STOC-1994-HerlihyS
- A simple constructive computability theorem for wait-free computation (MH, NS), pp. 243–252.
- STOC-1994-RajagopalanS #distributed
- A coding theorem for distributed computation (SR, LJS), pp. 790–799.
- CADE-1994-McPheeCG #geometry #proving #using
- Mechanically Proving Geometry Theorems Using a Combination of Wu’s Method and Collins’ Method (NFM, SCC, XSG), pp. 401–415.
- ICALP-1993-MichauxV #automaton
- Cobham’s Ttheorem seen through Büchi’s Theorem (CM, RV), pp. 325–334.
- ICALP-1993-Senizergues #effectiveness
- An Effective Version of Stallings’ Theorem in the Case of Context-Free Groups (GS), pp. 478–495.
- TLCA-1993-Groote #revisited
- The Conservation Theorem revisited (PdG), pp. 163–178.
- STOC-1993-GargVY #approximate #multi
- Approximate max-flow min-(multi)cut theorems and their applications (NG, VVV, MY), pp. 698–707.
- STOC-1993-HerlihyS
- The asynchronous computability theorem for t-resilient tasks (MH, NS), pp. 111–120.
- ICLP-1993-Turner #logic programming #source code
- A Monotonicity Theorem for Extended Logic Programs (HT), pp. 567–585.
CC-1992-KnoopS #interprocedural- The Interprocedural Coincidence Theorem (JK, BS), pp. 125–140.
- CADE-1992-AlexanderP #proving #similarity
- Proving Equality Theorems with Hyper-Linking (GDA, DAP), pp. 706–710.
- CADE-1992-ZhangH #induction #proving #set
- Proving the Chinese Remainder Theorem by the Cover Set Induction (HZ, XH), pp. 431–445.
- LICS-1992-GonthierLM #standard
- An abstract standardisation theorem (GG, JJL, PAM), pp. 72–81.
- ICALP-1991-GastinPZ #infinity
- A Kleene Theorem for Infinite Trace Languages (PG, AP, WZ), pp. 254–266.
- ICALP-1991-Wilke
- An Eilenberg Theorem for Infinity-Languages (TW), pp. 588–599.
- RTA-1991-Avenhaus #equation #induction #proving
- Proving Equational and Inductive Theorems by Completion and Embedding Techniques (JA), pp. 361–373.
ADC-1991-FerrariGM - An Extended Expansion Theorem (GLF, RG, UM), pp. 29–48.
- STOC-1991-Kilian #game studies
- A General Completeness Theorem for Two-Party Games (JK), pp. 553–560.
- LICS-1991-Kozen #algebra
- A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events (DK), pp. 214–225.
- POPL-1990-HeintzeJ #approximate #finite #logic programming #source code
- A Finite Presentation Theorem for Approximating Logic Programs (NH, JJ), pp. 197–209.
- STOC-1990-AlonST #graph
- A Separator Theorem for Graphs with an Excluded Minor and its Applications (NA, PDS, RT), pp. 293–299.
- STOC-1990-KirkpatrickMY #multi
- Quantitative Steinitz’s Theorems with Applications to Multifingered Grasping (DGK, BM, CKY), pp. 341–351.
- CSL-1990-Pudlak #bound
- Ramsey’s Theorem in Bounded Arithmetic (PP), pp. 308–317.
- PODS-1989-RamakrishnanSUV #program transformation
- Proof-Tree Transformation Theorems and Their Applications (RR, YS, JDU, MYV), pp. 172–181.
FPCA-1989-Wadler #exclamation #for free- Theorems for Free! (PW), pp. 347–359.
- CSL-1989-PasztorS
- A Streamlined Temporal Completeness Theorem (AP, IS), pp. 322–336.
- ICALP-1988-MehlhornY #how
- Constructive Hopf’s Theorem: Or How to Untangle Closed Planar Curves (KM, CKY), pp. 410–423.
- ALP-1988-HofbauerK #induction #proving #term rewriting
- Proving Inductive Theorems Based on Term Rewriting Systems (DH, RDK), pp. 180–190.
- STOC-1988-Ben-OrGW #distributed #fault tolerance
- Completeness Theorems for Non-Cryptographic Fault-Tolerant Distributed Computation (MBO, SG, AW), pp. 1–10.
- ICALP-1987-Kuich
- The Kleene and the Parikh Theorem in Complete Semirings (WK), pp. 212–225.
- STOC-1987-GoldreichMW #game studies #how #protocol
- How to Play any Mental Game or A Completeness Theorem for Protocols with Honest Majority (OG, SM, AW), pp. 218–229.
- ICALP-1986-Regan #reduction
- A Uniform Reduction Theorem — Extending a Result of J. Grollmann and A. Selman (KWR), pp. 324–333.
- POPL-1986-LengauerH #concurrent #network #sorting
- A Mechanically Certified Theorem about Optimal Concurrency of Sorting Networks (CL, CHH), pp. 307–317.
- ICALP-1985-Coppo #recursion
- A Completeness Theorem for Recursively Defined Types (MC), pp. 120–129.
- ICALP-1985-Hansel #proving
- A Simple Proof of the Skolem-Mahler-Lech Theorem (GH), pp. 244–249.
- ICALP-1985-Hortala-GonzalezR #hoare #logic #nondeterminism #source code #standard
- Hoare’s Logic for Nondeterministic Regular Programs: A Nonstandard Completeness Theorem (MTHG, MRA), pp. 270–280.
- STOC-1984-AjtaiB #constant #probability
- A Theorem on Probabilistic Constant Depth Computations (MA, MBO), pp. 471–474.
- ICALP-1982-Brandenburg
- Extended Chomsky-Schützenberger Theorems (FJB), pp. 83–93.
- ICALP-1982-KrevnerY #precedence
- An Iteration Theorem for Simple Precedence Languages (YK, AY), pp. 360–368.
- STOC-1981-Leivant #complexity #independence #parametricity #polymorphism #programming language
- The Complexity of Parameter Passing in Polymorphic Procedures (or: Programming Language Theorems Independent of Very Strong Theories) (DL), pp. 38–45.
- ICALP-1980-Kozen #modelling #representation
- A Representation Theorem for Models of *-Free PDL (DK), pp. 351–362.
- ICALP-1979-Istrail #fixpoint #monad #recursion #semantics #source code
- A Fixed-Point Theorem for Recursive-Enumerable Languages and Some Considerations About Fixed-Point Semantics of Monadic Programs (SI), pp. 289–303.
- ICALP-1979-Jeanrond #axiom #commutative #termination
- A Unique Termination Theorem for a Theory with Generalised Commutative Axioms (HJJ), pp. 316–330.
- STOC-1979-ODonnell #independence #programming language
- A Programming Language Theorem Which Is Independent of Peano Arithmetic (MO), pp. 176–188.
- POPL-1977-DeMilloLP #process #proving #social #source code
- Social Processes and Proofs of Theorems and Programs (RAD, RJL, AJP), pp. 206–214.
- STOC-1977-Beatty #ll
- Iteration Theorems for LL(k) Languages (JCB), pp. 122–131.
- STOC-1975-Perrault #transducer
- Intercalation Theorems for Tree Transducer Languages (CRP), pp. 126–136.
- ICALP-1974-Leeuwen #formal method
- A Generalisation of Parikh’s Theorem in Formal Language Theory (JvL), pp. 17–26.
- ICALP-1972-Vilfan
- A Generalization of a Theorem of Specker and Some Applications (BV), pp. 609–622.
- STOC-1971-Boasson
- An Iteration Theorem for One-Counter Languages (LB), pp. 116–120.
- STOC-1970-Rosen
- Tree-Manipulating Systems and Church-Rosser Theorems (BKR), pp. 117–127.
- STOC-1970-Rounds #proving
- Tree-Oriented Proofs of Some Theorems on Context-Free and Indexed Languages (WCR), pp. 109–116.
- STOC-1970-Ullian #product line
- Three Theorems on Abstract Families of Languages (JSU), pp. 226–230.
- STOC-1969-Ogden #stack
- Intercalation Theorems for Stack Languages (WFO), pp. 31–42.
