## Stem theorem$ (all stems)

### 515 papers:

- STOC-2015-Barman #approximate #nash #theorem
- Approximating Nash Equilibria and Dense Bipartite Subgraphs via an Approximate Version of Caratheodory’s Theorem (SB), pp. 361–369.
- STOC-2015-Chuzhoy #grid #theorem
- Excluded Grid Theorem: Improved and Simplified (JC), pp. 645–654.
- STOC-2015-KawarabayashiK #grid #theorem
- The Directed Grid Theorem (KiK, SK), pp. 655–664.
- ICALP-v2-2015-Finkel #automaton #infinity #scalability #theorem #word
- Incompleteness Theorems, Large Cardinals, and Automata over Infinite Words (OF), pp. 222–233.
- ICALP-v2-2015-KawarabayashiK #graph #theorem #towards
- Towards the Graph Minor Theorems for Directed Graphs (KiK, SK), pp. 3–10.
- LATA-2015-BabariD #automaton #logic #theorem
- A Nivat Theorem for Weighted Picture Automata and Weighted MSO Logic (PB, MD), pp. 703–715.
- LATA-2015-LuckMS #complexity #theorem
- Parameterized Complexity of CTL — A Generalization of Courcelle’s Theorem (ML, AM, IS), pp. 549–560.
- ICML-2015-KairouzOV #composition #difference #privacy #theorem
- The Composition Theorem for Differential Privacy (PK, SO, PV), pp. 1376–1385.
- CADE-2015-BackemanR #bound #proving #theorem proving
- Theorem Proving with Bounded Rigid E-Unification (PB, PR), pp. 572–587.
- CADE-2015-Baumgartner #named #proving #theorem proving
- SMTtoTPTP — A Converter for Theorem Proving Formats (PB), pp. 285–294.
- CADE-2015-BaumgartnerBW #named #proving #theorem proving
- Beagle — A Hierarchic Superposition Theorem Prover (PB, JB, UW), pp. 367–377.
- CADE-2015-FultonMQVP #axiom #hybrid #proving #theorem proving
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (NF, SM, JDQ, MV, AP), pp. 527–538.
- CADE-2015-HouGT #automation #logic #proving #theorem proving
- Automated Theorem Proving for Assertions in Separation Logic with All Connectives (ZH, RG, AT), pp. 501–516.
- CADE-2015-MouraKADR #agile #proving #theorem proving
- The Lean Theorem Prover (System Description) (LMdM, SK, JA, FvD, JvR), pp. 378–388.
- CSL-2015-KontinenMSV #semantics #theorem
- A Van Benthem Theorem for Modal Team Semantics (JK, JSM, HS, HV), pp. 277–291.
- FoSSaCS-2014-AdamekMMU #theorem
- Generalized Eilenberg Theorem I: Local Varieties of Languages (JA, SM, RSRM, HU), pp. 366–380.
- STOC-2014-ChekuriC #bound #polynomial #theorem
- Polynomial bounds for the grid-minor theorem (CC, JC), pp. 60–69.
- STOC-2014-KawarabayashiKK #graph #grid #problem #theorem
- 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 #theorem
- A characterization of locally testable affine-invariant properties via decomposition theorems (YY), pp. 154–163.
- DLT-J-2013-DrosteV14 #context-free grammar #theorem
- The Chomsky-SCHüTzenberger Theorem for Quantitative Context-Free Languages (MD, HV), pp. 955–970.
- DLT-J-2013-GocRRS14 #automation #on the #word
- On the number of Abelian Bordered Words (with an Example of Automatic Theorem-Proving) (DG, NR, MR, PS), pp. 1097–1110.
- DLT-2014-KarhumakiSZ #equivalence #theorem
- Variations of the Morse-Hedlund Theorem for k-Abelian Equivalence (JK, AS, LQZ), pp. 203–214.
- ICALP-v2-2014-DrosteP #automaton #distance #logic #theorem
- A Nivat Theorem for Weighted Timed Automata and Weighted Relative Distance Logic (MD, VP), pp. 171–182.
- IFM-2014-ChaudhariD #automation #proving #theorem proving
- Automated Theorem Prover Assisted Program Calculations (DLC, OPD), pp. 205–220.
- ICML-c2-2014-ArgyriouD #theorem
- A Unifying View of Representer Theorems (AA, FD), pp. 748–756.
- PPDP-2014-AotoS #induction #proving #theorem
- Decision Procedures for Proving Inductive Theorems without Induction (TA, SS), pp. 237–248.
- PPDP-2014-MehnerSSV #functional #parametricity #proving #theorem
- Parametricity and Proving Free Theorems for Functional-Logic Languages (SM, DS, LS, JV), pp. 19–30.
- POPL-2014-AccattoliBKL #standard #theorem
- A nonstandard standardization theorem (BA, EB, DK, CL), pp. 659–670.
- POPL-2014-Atkey #parametricity #theorem
- From parametricity to conservation laws, via Noether’s theorem (RA), pp. 491–502.
- SPLC-2014-ThumMBHRS #model checking #product line #proving #theorem proving
- Potential synergies of theorem proving and model checking for software product lines (TT, JM, FB, MH, AvR, GS), pp. 177–186.
- CAV-2014-Voronkov #architecture #first-order #named #proving #theorem proving
- AVATAR: The Architecture for First-Order Theorem Provers (AV), pp. 696–710.
- IJCAR-2014-BaumgartnerBW #finite #proving #quantifier #theorem proving
- Finite Quantification in Hierarchic Theorem Proving (PB, JB, UW), pp. 152–167.
- IJCAR-2014-BeyersdorffC #complexity #proving #theorem proving
- The Complexity of Theorem Proving in Circumscription and Minimal Entailment (OB, LC), pp. 403–417.
- IJCAR-2014-GoreTW #logic #proving #theorem proving #using
- A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description (RG, JT, JW), pp. 262–268.
- LICS-CSL-2014-BojanczykDK #calculus #composition #model checking #theorem #μ-calculus
- Decomposition theorems and model-checking for the modal μ-calculus (MB, CD, SK), p. 10.
- LICS-CSL-2014-HarwathHS #bound #composition #theorem
- Preservation and decomposition theorems for bounded degree structures (FH, LH, NS), p. 10.
- LICS-CSL-2014-Mahboubi #order #proving #theorem
- Computer-checked mathematics: a formal proof of the odd order theorem (AM), p. 1.
- RTA-TLCA-2014-BerardiS #theorem
- Ramsey Theorem as an Intuitionistic Property of Well Founded Relations (SB, SS), pp. 93–107.
- SAT-2014-IstrateC #complexity #proving #theorem
- Proof Complexity and the Kneser-Lovász Theorem (GI, AC), pp. 138–153.
- STOC-2013-BrandaoH #metric #quantum #theorem
- Quantum de finetti theorems under local measurements with applications (FGSLB, AWH), pp. 861–870.
- STOC-2013-LeeMM #theorem
- A node-capacitated okamura-seymour theorem (JRL, MM, MM), pp. 495–504.
- STOC-2013-SinclairS #complexity #theorem
- Lee-Yang theorems and the complexity of computing averages (AS, PS), pp. 625–634.
- CIAA-J-2012-GocHS13 #automation #combinator #word
- Automatic Theorem-Proving in Combinatorics on Words (DG, DH, JS), pp. 781–798.
- DLT-J-2012-KarhumakiPS13 #theorem
- Fine and Wilf’s Theorem for k-Abelian Periods (JK, SP, AS), pp. 1135–1152.
- CIAA-2013-ChistikovM #theorem #word
- A Uniformization Theorem for Nested Word to Word Transductions (DVC, RM), pp. 97–108.
- DLT-2013-DrosteV #context-free grammar #theorem
- The Chomsky-Schützenberger Theorem for Quantitative Context-Free Languages (MD, HV), pp. 203–214.
- ICALP-v1-2013-ODonnellT #composition #fourier #theorem
- 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 #theorem
- Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs (GB, FO), pp. 49–60.
- ICFP-2013-Morihata #parallel #theorem
- A short cut to parallelization theorems (AM), pp. 245–256.
- ICML-c1-2013-YuCSS #theorem
- Characterizing the Representer Theorem (YY, HC, DS, CS), pp. 570–578.
- LOPSTR-2013-AransayD #algebra #algorithm #execution #formal method #linear #theorem
- Formalization and Execution of Linear Algebra: From Theorems to Algorithms (JA, JD), pp. 1–18.
- POPL-2013-Gonthier #order #proving #theorem
- Engineering mathematics: the odd order theorem proof (GG), pp. 1–2.
- POPL-2013-ParkSP #proving #theorem proving
- A theorem prover for Boolean BI (JP, JS, SP), pp. 219–232.
- CADE-2013-HawblitzelKLR #automation #proving #source code #theorem proving #towards #using
- Towards Modularly Comparing Programs Using Automated Theorem Provers (CH, MK, SKL, HR), pp. 282–299.
- CAV-2013-KovacsV #first-order #proving #theorem proving
- First-Order Theorem Proving and Vampire (LK, AV), pp. 1–35.
- LICS-2013-FacchiniVZ #calculus #theorem #μ-calculus
- A Characterization Theorem for the Alternation-Free Fragment of the Modal μ-Calculus (AF, YV, FZ), pp. 478–487.
- SAT-2013-Beyersdorff #complexity #logic #proving #theorem proving
- The Complexity of Theorem Proving in Autoepistemic Logic (OB), pp. 365–376.
- SAT-2013-Lauria #bound #proving #rank #theorem
- A Rank Lower Bound for Cutting Planes Proofs of Ramsey’s Theorem (ML), pp. 351–364.
- TLCA-2013-KrausECA #theorem
- Generalizations of Hedberg’s Theorem (NK, MHE, TC, TA), pp. 173–188.
- STOC-2012-GroheM #graph #morphism #theorem
- Structure theorem and isomorphism test for graphs with excluded topological subgraphs (MG, DM), pp. 173–192.
- STOC-2012-MosselR #theorem
- A quantitative gibbard-satterthwaite theorem without neutrality (EM, MZR), pp. 1041–1060.
- CIAA-2012-GocHS #automation #combinator #word
- Automatic Theorem-Proving in Combinatorics on Words (DG, DH, JS), pp. 180–191.
- DLT-2012-KapoutsisL #automaton #finite #nondeterminism #theorem
- Analogs of Fagin’s Theorem for Small Nondeterministic Finite Automata (CAK, NL), pp. 202–213.
- DLT-2012-KarhumakiPS #theorem
- Fine and Wilf’s Theorem for k-Abelian Periods (JK, SP, AS), pp. 296–307.
- DLT-2012-Okhotin #theorem
- Non-erasing Variants of the Chomsky-Schützenberger Theorem (AO), pp. 121–129.
- ICFP-2012-StewartBA #proving #theorem proving
- Verified heap theorem prover by paramodulation (GS, LB, AWA), pp. 3–14.
- POPL-2012-Moore #proving #theorem proving
- Meta-level features in an industrial-strength theorem prover (JSM), pp. 425–426.
- CSL-2012-Rabinovich #proving #theorem
- A Proof of Kamp’s theorem (AR), pp. 516–527.
- ICLP-J-2012-BabbL #modelling #theorem
- Module theorem for the general theory of stable models (JB, JL), pp. 719–735.
- IJCAR-2012-JacquelBDD #automation #deduction #modulo theories #proving #theorem proving #using #verification
- Tableaux Modulo Theories Using Superdeduction — An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover (MJ, KB, DD, CD), pp. 332–338.
- LICS-2012-ChenM #algebra #category theory #constraints #quantifier #theorem
- An Algebraic Preservation Theorem for Aleph-Zero Categorical Quantified Constraint Satisfaction (HC, MM), pp. 215–224.
- LICS-2012-TraytelPB #category theory #composition #data type #higher-order #logic #proving #theorem proving
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (DT, AP, JCB), pp. 596–605.
- RTA-2012-Accattoli #theorem
- An Abstract Factorization Theorem for Explicit Substitutions (BA), pp. 6–21.
- TACAS-2011-ChamarthiDMV #proving #theorem proving
- The ACL2 Sedan Theorem Proving System (HRC, PCD, PM, DV), pp. 291–295.
- PLDI-2011-PerezR #calculus #logic #proving #theorem proving
- Separation logic + superposition calculus = heap theorem prover (JANP, AR), pp. 556–566.
- STOC-2011-BodirskyP #graph #theorem
- Schaefer’s theorem for graphs (MB, MP), pp. 655–664.
- STOC-2011-Sherstov #communication #complexity #quantum #query #theorem
- Strong direct product theorems for quantum communication and query complexity (AAS), pp. 41–50.
- DLT-J-2009-BrzozowskiGS11 #formal method #theorem
- Closures in Formal Languages and Kuratowski’s Theorem (JAB, EG, JS), pp. 301–321.
- DLT-J-2009-GazdagN11 #theorem
- A Kleene Theorem for Bisemigroup and binoid Languages (ZG, ZLN), pp. 427–446.
- DLT-2011-Shallit #revisited #theorem
- Fife’s Theorem Revisited (JS), pp. 397–405.
- ICALP-v2-2011-Delacourt #automaton #set #theorem
- Rice’s Theorem for μ-Limit Sets of Cellular Automata (MD), pp. 89–100.
- SEFM-2011-ErnstSR #analysis #empirical #interactive #proving #theorem proving #verification
- Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving (GE, GS, WR), pp. 188–203.
- SEFM-2011-JacquelBDD #automation #proving #theorem proving #using #verification
- Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving (MJ, KB, DD, CD), pp. 253–268.
- ICFP-2011-MuM #functional #morphism #theorem
- Generalising and dualising the third list-homomorphism theorem: functional pearl (SCM, AM), pp. 385–391.
- OOPSLA-2011-DelawareCB #product line #theorem
- Product lines of theorems (BD, WRC, DSB), pp. 595–608.
- GPCE-2011-Launchbury
- Theorem-based circuit derivation in cryptol (JL), pp. 185–186.
- CADE-2011-AspertiRCT #interactive #proving #theorem proving
- The Matita Interactive Theorem Prover (AA, WR, CSC, ET), pp. 64–69.
- CADE-2011-Brown #higher-order #problem #proving #satisfiability #sequence #theorem proving
- Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems (CEB), pp. 147–161.
- CADE-2011-SchneiderS #automation #first-order #ontology #owl #proving #reasoning #theorem proving #using
- Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving (MS, GS), pp. 461–475.
- RTA-2011-AotoYC #higher-order #induction #theorem
- Natural Inductive Theorems for Higher-Order Rewriting (TA, TY, YC), pp. 107–121.
- TLCA-2011-ManzonettoP #theorem #λ-calculus
- Böhm’s Theorem for Resource λ Calculus through Taylor Expansion (GM, MP), pp. 153–168.
- STOC-2010-KawarabayashiW #algorithm #graph #proving #theorem
- A shorter proof of the graph minor algorithm: the unique linkage theorem (KiK, PW), pp. 687–694.
- STOC-2010-Klauck #theorem
- A strong direct product theorem for disjointness (HK), pp. 77–86.
- FLOPS-2010-SeidelV #automation #generative #theorem
- Automatically Generating Counterexamples to Naive Free Theorems (DS, JV), pp. 175–190.
- AFL-J-2008-Blanchet-SadriOR10 #theorem #word
- Fine and Wilf’s Theorem for Partial Words with Arbitrarily Many Weak Periods (FBS, TO, TDR), pp. 705–722.
- CIAA-2010-Grosu #commutative #theorem
- The Cayley-Hamilton Theorem for Noncommutative Semirings (RG), pp. 143–153.
- DLT-2010-DrosteV #automaton #bound #logic #multi #theorem
- 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 #theorem
- Graph Homomorphisms with Complex Values: A Dichotomy Theorem (JyC, XC, PL), pp. 275–286.
- ICALP-v1-2010-LeeZ #communication #complexity #composition #theorem
- Composition Theorems in Communication Complexity (TL, SZ), pp. 475–489.
- ICALP-v1-2010-Xia #artificial reality #reduction #theorem
- Holographic Reduction: A Domain Changed Application and Its Partial Converse Theorems (MX), pp. 666–677.
- ICPR-2010-DursunDG #2d #image #re-engineering #slicing #theorem
- Paired Transform Slice Theorem of 2-D Image Reconstruction from Projections (SD, ND, AMG), pp. 2395–2398.
- KEOD-2010-KatsumiG #lifecycle #ontology #proving #theorem proving
- Theorem Proving in the Ontology Lifecycle (MK, MG), pp. 37–49.
- PPDP-2010-Bonacina #on the #proving #theorem proving
- On theorem proving for program checking: historical perspective and recent developments (MPB), pp. 1–12.
- IJCAR-2010-BaeldeMS #induction #proving #theorem proving
- Focused Inductive Theorem Proving (DB, DM, ZS), pp. 278–292.
- IJCAR-2010-KorovinS #named #proving #similarity #theorem proving
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality (KK, CS), pp. 196–202.
- LICS-2010-Moore #proving #theorem proving #verification
- Theorem Proving for Verification: The Early Days (JSM), p. 283.
- TAP-2010-Rusu #proving #specification #theorem proving
- Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications (VR), pp. 135–150.
- SIGMOD-2009-Kifer #privacy #theorem
- Attacks on privacy and deFinetti’s theorem (DK), pp. 127–138.
- FASE-2009-KovacsV #array #invariant #proving #source code #theorem proving #using
- Finding Loop Invariants for Programs over Arrays Using a Theorem Prover (LK, AV), pp. 470–485.
- FoSSaCS-2009-BonsangueRS #algebra #polynomial #theorem
- A Kleene Theorem for Polynomial Coalgebras (MMB, JJMMR, AS), pp. 122–136.
- DLT-2009-BrzozowskiGS #formal method #theorem
- Closures in Formal Languages and Kuratowski’s Theorem (JAB, EG, JS), pp. 125–144.
- DLT-2009-Saarela #complexity #equation #on the #satisfiability #theorem
- On the Complexity of Hmelevskii’s Theorem and Satisfiability of Three Unknown Equations (AS), pp. 443–453.
- ICALP-v1-2009-GuhaH #bound #order #random #theorem
- 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 #theorem
- On a Network Generalization of the Minmax Theorem (CD, CHP), pp. 423–434.
- LATA-2009-Strassburger #theorem
- A Kleene Theorem for Forest Languages (LS), pp. 715–727.
- ICFP-2009-Voigtlander #functional #theorem
- Free theorems involving type constructor classes: functional pearl (JV), pp. 173–184.
- POPL-2009-MorihataMHT #divide and conquer #morphism #theorem
- 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 #theorem #using
- Formalizing Desargues’ theorem in Coq using ranks (NM, JN, PS), pp. 1110–1115.
- CADE-2009-BensaidCP #integer #named #proving #theorem proving
- Dei: A Theorem Prover for Terms with Integer Exponents (HB, RC, NP), pp. 146–150.
- CADE-2009-BoigelotBL #automaton #theorem
- A Generalization of Semenov’s Theorem to Automata over Real Numbers (BB, JB, JL), pp. 469–484.
- CADE-2009-BonacinaLM #on the #proving #satisfiability #theorem proving
- On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving (MPB, CL, LMdM), pp. 35–50.
- CADE-2009-McLaughlinP #performance #proving #theorem proving
- Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method (SM, FP), pp. 230–244.
- CADE-2009-Stickel #proving #theorem proving
- Building Theorem Provers (MES), pp. 306–321.
- CADE-2009-SutcliffeBBT #automation #development #higher-order #logic #proving #theorem proving
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic (GS, CB, CEB, FT), pp. 116–130.
- CADE-2009-SwiderskiPGFS #analysis #dependence #induction #proving #termination #theorem proving
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving (SS, MP, JG, CF, PSK), pp. 322–338.
- CSL-2009-Moschovakis #recursion #theorem
- Kleene’s Amazing Second Recursion Theorem (YNM), pp. 24–39.
- TestCom-FATES-2009-SubramaniamXGP #approach #proving #testing #theorem proving #using
- An Approach for Test Selection for EFSMs Using a Theorem Prover (MS, LX, BG, ZP), pp. 146–162.
- TLCA-2009-Pagani #difference #theorem
- The Cut-Elimination Theorem for Differential Nets with Promotion (MP), pp. 219–233.
- ESOP-2008-MatthewsA #exclamation #morphism #parametricity #polymorphism #runtime #theorem
- Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices! (JM, AA), pp. 16–31.
- FoSSaCS-2008-DrosteQ #automaton #theorem
- A Kleene-Schützenberger Theorem for Weighted Timed Automata (MD, KQ), pp. 142–156.
- PEPM-2008-Voigtlander #correctness #proving #theorem
- Proving correctness via free theorems: the case of the destroy/build-rule (JV), pp. 13–20.
- STOC-2008-BorgsCIKMP #theorem
- The myth of the folk theorem (CB, JTC, NI, ATK, VSM, CHP), pp. 365–372.
- STOC-2008-ImpagliazzoJKW #theorem
- Uniform direct product theorems: simplified, optimized, and derandomized (RI, RJ, VK, AW), pp. 579–588.
- STOC-2008-JainKN #bound #communication #complexity #theorem
- Direct product theorems for classical communication complexity via subdistribution bounds: extended abstract (RJ, HK, AN), pp. 599–608.
- STOC-2008-Nandakumar #effectiveness #theorem
- An effective ergodic theorem and some applications (SN), pp. 39–44.
- AFL-2008-GazdagN #theorem
- A Kleene Theorem for Binoid Languages (ZG, ZLN), pp. 170–182.
- DLT-2008-KarhumakiS #analysis #theorem
- An Analysis and a Reproof of Hmelevskii’s Theorem (JK, AS), pp. 467–478.
- ICALP-A-2008-LeeM #programming #theorem
- Product Theorems Via Semidefinite Programming (TL, RM), pp. 674–685.
- ICALP-B-2008-YokoyamaAG #theorem
- Reversible Flowchart Languages and the Structured Reversible Program Theorem (TY, HBA, RG), pp. 258–270.
- LATA-2008-Steinberg #matrix #sequence #theorem
- Subsequence Counting, Matrix Representations and a Theorem of Eilenberg (BS), pp. 6–10.
- SEFM-2008-GuoS #finite #impact analysis #proving #state machine #theorem proving #using
- Formal Change Impact Analyses of Extended Finite State Machines Using a Theorem Prover (BG, MS), pp. 335–344.
- IFL-2008-Hinze #proving #theorem
- Scans and Convolutions — A Calculational Proof of Moessner’s Theorem (RH), pp. 1–24.
- ICGT-2008-Pennemann #proving #theorem proving
- Resolution-Like Theorem Proving for High-Level Conditions (KHP), pp. 289–304.
- BX-2008-Voigtlaender1 #bidirectional #theorem
- Free Theorems and Bidirectional Transformations (JV), p. 30.
- POPL-2008-Asperti #theorem
- The intensional content of Rice’s theorem (AA), pp. 113–119.
- SAC-2008-AbedMS #analysis #graph #multi #proving #reachability #theorem proving #using
- Reachability analysis using multiway decision graphs in the HOL theorem prover (SA, OAM, GAS), pp. 333–338.
- SAC-2008-Michelucci #geometry #proving #theorem #word
- Isometry group, words and proofs of geometric theorems (DM), pp. 1821–1825.
- CAV-2008-Harrison #proving #theorem proving #tutorial #verification
- Theorem Proving for Verification (Invited Tutorial) (JH), pp. 11–18.
- CAV-2008-JoshiK #graph transformation #theorem #verification
- Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems (SJ, BK), pp. 214–226.
- ICLP-2008-NearBF #declarative #first-order #logic #named #proving #theorem proving
- αleanTAP: A Declarative Theorem Prover for First-Order Classical Logic (JPN, WEB, DPF), pp. 238–252.
- IJCAR-2008-BenzmullerPTF #automation #higher-order #logic #named #proving #theorem proving
- LEO-II — A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) (CB, LCP, FT, AF), pp. 162–170.
- IJCAR-2008-Gacek #interactive #proving #theorem proving
- The Abella Interactive Theorem Prover (System Description) (AG), pp. 154–161.
- IJCAR-2008-Korovin #first-order #logic #named #proving #theorem proving
- iProver — An Instantiation-Based Theorem Prover for First-Order Logic (System Description) (KK), pp. 292–298.
- IJCAR-2008-Otten #agile #logic #performance #proving #theorem proving
- leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) (JO), pp. 283–291.
- IJCAR-2008-PlatzerQ #hybrid #named #proving #theorem proving
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) (AP, JDQ), pp. 171–178.
- LICS-2008-Duris #theorem
- Hypergraph Acyclicity and Extension Preservation Theorems (DD), pp. 418–427.
- STOC-2007-PassV #game studies #parallel #performance #theorem
- An efficient parallel repetition theorem for Arthur-Merlin games (RP, MV), pp. 420–429.
- ICALP-2007-BoigelotB #automaton #theorem
- A Generalization of Cobham’s Theorem to Automata over Real Numbers (BB, JB), pp. 813–824.
- ICALP-2007-Colcombet #combinator #theorem
- A Combinatorial Theorem for Trees (TC), pp. 901–912.
- SAC-2007-Dufourd #framework #proving #theorem
- A hypermap framework for computer-aided proofs in surface subdivisions: genus theorem and Euler’s formula (JFD), pp. 757–761.
- CADE-2007-TiwariG #logic #program analysis #proving #theorem proving #using
- Logical Interpretation: Static Program Analysis Using Theorem Proving (AT, SG), pp. 147–166.
- CSL-2007-WeisI #strict #theorem #word
- Structure Theorem and Strict Alternation Hierarchy for FO2 on Words (PW, NI), pp. 343–357.
- LICS-2007-CateBV #first-order #logic #theorem
- Lindstrom theorems for fragments of first-order logic (BtC, JvB, JAV), pp. 280–292.
- LICS-2007-NguyenC #complexity #proving #theorem
- The Complexity of Proving the Discrete Jordan Curve Theorem (PN, SAC), pp. 245–256.
- VMCAI-2007-BouillaguetKWZR #data type #first-order #proving #theorem proving #using #verification
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System (CB, VK, TW, KZ, MCR), pp. 74–88.
- ASE-2006-Jurjens #analysis #automation #java #proving #security #source code #theorem proving #using
- Security Analysis of Crypto-based Java Programs using Automated Theorem Provers (JJ), pp. 167–176.
- STOC-2006-AmbainisSW #bound #quantum #theorem #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 #theorem
- The PCP theorem by gap amplification (ID), pp. 241–250.
- DLT-J-2005-BesC06 #linear #order #theorem #word
- A Kleene Theorem for Languages of Words Indexed by Linear Orderings (AB, OC), pp. 519–542.
- FM-2006-UmenoL #automaton #case study #protocol #proving #safety #theorem proving #using
- Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study (SU, NAL), pp. 64–80.
- SFM-2006-Harrison #float #proving #theorem proving #using #verification
- Floating-Point Verification Using Theorem Proving (JH), pp. 211–242.
- SFM-2006-Manolios #proving #refinement #theorem proving
- Refinement and Theorem Proving (PM), pp. 176–210.
- ICPR-v2-2006-HuD #classification #multi #theorem
- A “No Panacea Theorem” for Multiple Classifier Combination (RH, RID), pp. 1250–1253.
- ICPR-v3-2006-TanakaFKI #theorem
- A Theoretical and Experimental Consideration on Interference in Resolutions between Sampling Theorem and OK-Quantization Theory (YT, TF, HK, TI), pp. 869–872.
- ICSE-2006-ManoliosV #proving #static analysis #termination #theorem proving
- Integrating static analysis and general-purpose theorem proving for termination analysis (PM, DV), pp. 873–876.
- CAV-2006-Roe #heuristic #modulo theories #proving #smt #theorem proving
- The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover (KR), pp. 467–470.
- ISSTA-2006-YorshBS #abstraction #exclamation #proving #testing #theorem proving
- Testing, abstraction, theorem proving: better together! (GY, TB, MS), pp. 145–156.
- SAT-2006-ChenIJSS #constraints #problem #theorem
- A Dichotomy Theorem for Typed Constraint Satisfaction Problems (SC, TI, KJ, DS, MS), pp. 226–239.
- ASE-2005-WardKA #framework #named #proving #theorem proving
- Prufrock: a framework for constructing polytypic theorem provers (JW, GK, PA), pp. 423–426.
- TACAS-2005-IsobeR #csp #proving #refinement #theorem proving
- A Generic Theorem Prover of CSP Refinement (YI, MR), pp. 108–123.
- TACAS-2005-LeinoMO #proving #quantifier #theorem proving
- A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover (KRML, MM, XO), pp. 334–348.
- DLT-2005-BedonR #linear #order #theorem #word
- Schützenberger and Eilenberg Theorems for Words on Linear Orderings (NB, CR), pp. 134–145.
- DLT-2005-BesC #linear #order #theorem #word
- A Kleene Theorem for Languages of Words Indexed by Linear Orderings (AB, OC), pp. 158–167.
- ICFP-2005-ChenX #programming #proving #theorem proving
- Combining programming with theorem proving (CC, HX), pp. 66–77.
- CADE-2005-ChaudhuriP #first-order #linear #logic #proving #theorem proving
- A Focusing Inverse Method Theorem Prover for First-Order Linear Logic (KC, FP), pp. 69–83.
- CAV-2005-CookKS #named #proving #theorem proving #verification
- Cogent: Accurate Theorem Proving for Program Verification (BC, DK, NS), pp. 296–300.
- CSL-2005-Berger #normalisation #theorem
- An Abstract Strong Normalization Theorem (UB), pp. 27–35.
- LICS-2005-DawarO #theorem
- Modal Characterisation Theorems over Special Classes of Frames (AD, MO), pp. 21–30.
- TLCA-2005-Coquand #theorem #λ-calculus
- Completeness Theorems and λ-Calculus (TC), pp. 1–9.
- TACAS-2004-McMillan #proving #theorem proving
- An Interpolating Theorem Prover (KLM), pp. 16–30.
- PLDI-2004-Appel #process #proving #revisited #social #source code #theorem
- Social processes and proofs of theorems and programs, revisited (AWA), p. 170.
- STOC-2004-ChenKLRSV #bound #confluence #theorem
- (Almost) tight bounds and existence theorems for confluent flows (JC, RDK, LL, RR, RS, AV), pp. 529–538.
- STOC-2004-CorreaG #approximate #graph #theorem
- An approximate König’s theorem for edge-coloring weighted bipartite graphs (JRC, MXG), pp. 398–406.
- STOC-2004-Obata #approximate #multi #theorem
- Approximate max-integral-flow/min-multicut theorems (KO), pp. 539–545.
- CIAA-2004-Maletti #theorem #transducer
- Myhill-Nerode Theorem for Sequential Transducers over Unique GCD-Monoids (AM), pp. 323–324.
- DLT-2004-GenestMK #algorithm #automaton #communication #effectiveness #theorem
- A Kleene Theorem for a Class of Communicating Automata with Effective Algorithms (BG, AM, DK), pp. 30–48.
- ICALP-2004-EdalatP #theorem
- A Domain Theoretic Account of Picard’s Theorem (AE, DP), pp. 494–505.
- ICALP-2004-Meer #proving #theorem
- Transparent Long Proofs: A First PCP Theorem for NPR (KM), pp. 959–970.
- ICALP-2004-Toftdal #analysis #effectiveness #logic #theorem
- A Calibration of Ineffective Theorems of Analysis in a Hierarchy of Semi-classical Logical Principles: (Extended Abstract) (MT), pp. 1188–1200.
- IFM-2004-EllisI #automation #integration #program analysis #proving #theorem proving
- An Integration of Program Analysis and Automated Theorem Proving (BJE, AI), pp. 67–86.
- IFM-2004-Melham #functional #model checking #proving #theorem proving
- Integrating Model Checking and Theorem Proving in a Reflective Functional Language (TFM), pp. 36–39.
- ICEIS-v1-2004-Augusto #model checking #theorem proving #verification
- Model Checking and Theorem Proving-Based Verification of EIS (JCA), p. XXXIII-XXXIV.
- POPL-2004-JohannV #theorem
- Free theorems in the presence of
*seq*(PJ, JV), pp. 99–110. - CAV-2004-BallCLZ #abstraction #automation #named #proving #refinement #theorem proving
- Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement (TB, BC, SKL, LZ), pp. 457–461.
- CSL-2004-DawsonG #termination #theorem
- A General Theorem on Termination of Rewriting (JED, RG), pp. 100–114.
- CSL-2004-GanzingerK #equation #proving #reasoning #theorem proving
- Integrating Equational Reasoning into Instantiation-Based Theorem Proving (HG, KK), pp. 71–84.
- CSL-2004-Lynch #proving #theorem proving
- Unsound Theorem Proving (CL), pp. 473–487.
- IJCAR-2004-ColtonMSM #algebra #automation #classification #finite #generative #theorem
- Automatic Generation of Classification Theorems for Finite Algebras (SC, AM, VS, RLM), pp. 400–414.
- IJCAR-2004-DenneyFS #automation #proving #theorem proving #using
- Using Automated Theorem Provers to Certify Auto-generated Aerospace Software (ED, BF, JS), pp. 198–212.
- IJCAR-2004-WintersteinBG #diagrams #proving #theorem proving
- Dr.Doodle: A Diagrammatic Theorem Prover (DW, AB, CAG), pp. 331–335.
- RTA-2004-AotoYT #higher-order #induction #theorem
- Inductive Theorems for Higher-Order Rewriting (TA, TY, YT), pp. 269–284.
- DRR-2003-CinqueLMR #theorem
- Fermat theorem and elliptic color histogram features (LC, SL, AM, FDR), pp. 234–240.
- DLT-2003-Borchardt #theorem
- The Myhill-Nerode Theorem for Recognizable Tree Series (BB), pp. 146–158.
- ICALP-2003-JainRS #communication #complexity #theorem
- A Direct Sum Theorem in Communication Complexity via Message Compression (RJ, JR, PS), pp. 300–315.
- SEFM-2003-DeharbeR #debugging #proving #theorem proving #verification
- Light-Weight Theorem Proving for Debugging and Verifying Units of Code (DD, SR), pp. 220–228.
- LOPSTR-2003-LehmannL #generative #induction #proving #theorem proving #using
- Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce (HL, ML), pp. 1–19.
- CADE-2003-AvenhausKSW #exclamation #how #induction #theorem
- How to Prove Inductive Theorems? QUODLIBET! (JA, UK, TSS, CPW), pp. 328–333.
- CADE-2003-DeplagneKKN #equation #induction #proving #theorem
- Proof Search and Proof Check for Equational and Inductive Theorems (ED, CK, HK, QHN), pp. 297–316.
- CAV-2003-FlanaganJOS #lazy evaluation #proving #theorem proving #using
- Theorem Proving Using Lazy Proof Explication (CF, RJ, XO, JBS), pp. 355–367.
- FATES-2003-HahnleW #proving #testing #theorem proving #using
- Using a Software Testing Technique to Improve Theorem Proving (RH, AW), pp. 30–41.
- LICS-2003-GanzingerK #proving #theorem proving
- New Directions in Instantiation-Based Theorem Proving (HG, KK), pp. 55–64.
- ICALP-2002-BonichonSM #theorem
- Wagner’s Theorem on Realizers (NB, BLS, MM), pp. 1043–1053.
- CADE-2002-Brown #higher-order #proving #set #theorem proving
- Solving for Set Variables in Higher-Order Theorem Proving (CEB), pp. 408–422.
- CADE-2002-Colton #generative #theorem
- The HR Program for Theorem Generation (SC), pp. 285–289.
- CADE-2002-MouraRS #bound #infinity #lazy evaluation #model checking #proving #theorem proving
- Lazy Theorem Proving for Bounded Model Checking over Infinite Domains (LMdM, HR, MS), pp. 438–455.
- CADE-2002-Paulson #case study #reasoning #theorem
- The Reflection Theorem: A Study in Meta-theoretic Reasoning (LCP), pp. 377–391.
- CAV-2002-Jacobi #model checking #pipes and filters #verification
- Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving (CJ0), pp. 309–323.
- LICS-2002-Otto #finite #theorem
- Modal and Guarded Characterisation Theorems over Finite Transition Systems (MO), p. 371–?.
- TestCom-2002-CastanetR #analysis #proving #reachability #testing #theorem proving
- Generate Certified Test Cases by Combining Theorem Proving and Reachability Analysis (RC, DR), pp. 249–266.
- IFL-2001-MolEP #functional #proving #theorem proving
- Theorem Proving for Functional Programmers (MdM, MCJDvE, MJP), pp. 55–71.
- CAV-2001-Bertot #formal method #proving #theorem proving #verification
- Formalizing a JVML Verifier for Initialization in a Theorem Prover (YB), pp. 14–24.
- CSL-2001-BaazM #on the #theorem
- On a Generalisation of Herbrand’s Theorem (MB, GM), pp. 469–483.
- CSL-2001-GalotaV #automaton #theorem
- A Generalization of the Büchi-Elgot-Trakhtenbrot Theorem (MG, HV), pp. 355–368.
- CSL-2001-GroheW #locality #theorem
- An Existential Locality Theorem (MG, SW), pp. 99–114.
- ICLP-2001-ErdemL #source code #theorem
- Fages’ Theorem for Programs with Nested Expressions (EE, VL), pp. 242–254.
- IJCAR-2001-Beeson #higher-order #proving #theorem proving
- A Second-Order Theorem Prover Applied to Circumscription (MB), pp. 318–324.
- IJCAR-2001-GanzingerM #bottom-up #logic programming #source code #theorem
- A New Meta-complexity Theorem for Bottom-Up Logic Programs (HG, DAM), pp. 514–528.
- IJCAR-2001-GieslK #decidability #induction #theorem
- Decidable Classes of Inductive Theorems (JG, DK), pp. 469–484.
- IJCAR-2001-Happe #proving #theorem proving
- The MODPROF Theorem Prover (JH), pp. 459–463.
- IJCAR-2001-HodasT #agile #first-order #implementation #linear #logic #named #proving #theorem proving
- lolliCop — A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic (JSH, NT), pp. 670–684.
- IJCAR-2001-LetzS #calculus #named #proving #theorem proving
- DCTP — A Disconnection Calculus Theorem Prover — System Abstract (RL, GS), pp. 381–385.
- IJCAR-2001-NieuwenhuisHRV #evaluation #on the #proving #theorem proving
- On the Evaluation of Indexing Techniques for Theorem Proving (RN, TH, AR, AV), pp. 257–271.
- IJCAR-2001-Pastre #deduction #knowledge-based #proving #theorem proving
- MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction (DP), pp. 685–689.
- IJCAR-2001-SchmittLKN #interactive #proving #theorem proving
- JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants (SS, LL, CK, AN), pp. 421–426.
- LICS-2001-CookK #higher-order #reasoning #theorem #using
- A Second-Order System for Polytime Reasoning Using Graedel’s Theorem (SAC, AK), pp. 177–186.
- SAT-2001-McllraithA #proving #theorem proving
- Theorem Proving with Structured Theories (Preliminary Report)* (SM, EA), pp. 311–328.
- STOC-2000-Kilian #theorem
- More general completeness theorems for secure two-party computation (JK), pp. 316–324.
- WLC-2000-Shoji #proving #theorem
- A Proof of Okninski, Putcha’s Theorem (KS), pp. 420–427.
- ICPR-v3-2000-ShenIT00a #2d #image #novel #symmetry #theorem
- A Novel Theorem on Symmetries of 2D Images (DS, HHSI, EKT), pp. 7014–7017.
- CADE-2000-AndrewsB #education #higher-order #logic #named #proving #theorem proving #tutorial #using
- Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic (PBA, CEB), pp. 511–512.
- CADE-2000-AndrewsBB #proving #theorem proving #type system
- System Description: TPS: A Theorem Proving System for Type Theory (PBA, MB, CEB), pp. 164–169.
- CADE-2000-Harrison #proving #theorem proving #using #verification
- High-Level Verification Using Theorem Proving and Formalized Mathematics (JH), pp. 1–6.
- CADE-2000-NeculaL #generative #proving #theorem proving
- Proof Generation in the Touchstone Theorem Prover (GCN, PL), pp. 25–44.
- CADE-2000-Seger #float #model checking #proving #theorem proving
- Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice (CJHS), p. 235.
- CADE-2000-Sinz #algebra #automation #proving #theorem proving
- System Description: ARA — An Automatic Theorem Prover for Relation Algebras (CS), pp. 177–182.
- CL-2000-HahnleHS #constraints #finite #generative #proving #theorem proving
- Moder Generation Theorem Proving with Finite Interval Constraints (RH, RH, YS), pp. 285–299.
- LICS-2000-Kripke #algorithm #first-order #theorem
- From the Church-Turing Thesis to the First-Order Algorithm Theorem (SK), p. 177.
- LICS-2000-McMillan #model checking #proving #theorem
- Some Strategies for Proving Theorems with a Model Checker (KLM), pp. 305–306.
- FASE-1999-LuthTKK #development #proving #theorem proving #tool support
- TAS and IsaWin: Tools for Transformational Program Development and Theorem Proving (CL, HT, K, BKB), pp. 239–243.
- TACAS-1999-RusuS #abstraction #on the #proving #safety #static analysis #theorem proving
- On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction (VR, ES), pp. 178–192.
- TACAS-1999-SpeltE #analysis #database #object-oriented #theorem proving
- A Theorem Prover-Based Analysis Tool for Object-Oriented Databases (DS, SE), pp. 375–389.
- STOC-1999-CaiNS #probability #theorem
- Hardness and Hierarchy Theorems for Probabilistic Quasi-Polynomial Time (JyC, AN, DS), pp. 726–735.
- STOC-1999-GalR #theorem
- A Theorem on Sensitivity and Applications in Private Computation (AG, AR), pp. 348–357.
- DLT-1999-KarhumakiM #fault #theorem
- Defect theorems for trees (JK, SM), pp. 164–177.
- FM-v2-1999-Nadjm-TehraniA #design #modelling #proving #theorem proving
- Combining Theorem Proving and Continuous Models in Synchronous Design (SNT, OÅ), pp. 1384–1399.
- CADE-1999-Artemov #on the #proving #theorem proving #verification
- On Explicit Reflection in Theorem Proving and Formal Verification (SNA), pp. 267–281.
- CADE-1999-FrankeK #automation #communication #distributed #proving #theorem proving
- System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving (AF, MK), pp. 217–221.
- CADE-1999-Hickey #distributed #fault tolerance #proving #theorem proving
- Fault-Tolerant Distributed Theorem Proving (JH), pp. 227–231.
- CADE-1999-HutterB #contest #design #induction #proving #theorem proving
- The Design of the CADE-16 Inductive Theorem Prover Contest (DH, AB), pp. 374–377.
- CADE-1999-JanicicBG #flexibility #framework #integration #proving #theorem proving
- A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers (PJ, AB, IG), pp. 127–141.
- CADE-1999-Nipkow #programming language #proving #theorem proving
- Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract) (TN), p. 398.
- CADE-1999-Voronkov #named #proving #theorem proving
- KK: a theorem prover for K (AV), pp. 383–387.
- CAV-1999-ManoliosNS #bisimulation #model checking #proving #theorem proving
- Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation (PM, KSN, RS), pp. 369–379.
- CSL-1999-Howe #interactive #proving #theorem proving #type system #using
- Interactive Theorem Proving Using Type Theory (DJH), p. 578.
- LICS-1999-HopkinsK #algebra #commutative #theorem
- Parikh’s Theorem in Commutative Kleene Algebra (MWH, DK), pp. 394–401.
- TLCA-1999-Statman #consistency #equation #theorem
- Consequences of Jacopini’s Theorem: Consistent Equalities and Equations (RS), pp. 355–364.
- ASE-1998-Ledru #identification #proving #theorem proving
- Identifying Pre-Conditions with the Z/EVES Theorem Prover (YL), p. 32–?.
- DAC-1998-AagaardJS #evaluation #industrial #proving #theorem proving
- Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment (MA, RBJ, CJHS), pp. 538–541.
- PODS-1998-SamoladasM #bound #multi #query #theorem
- A Lower Bound Theorem for Indexing Schemes and Its Application to Multidimensional Range Queries (VS, DPM), pp. 44–51.
- ITiCSE-1998-RodgerG #automaton #theorem
- JFLAP (poster): an aid to studying theorems in automata theory (SHR, EG), p. 302.
- CSMR-1998-JakobiW #automation #database #evaluation #framework #maintenance #named #proving #theorem proving
- DBFW: A Simple DataBase FrameWork for the Evaluation and Maintenance of Automated Theorem Prover Data (PJ, AW), pp. 185–188.
- STOC-1998-Bshouty #algorithm #composition #learning #theorem
- A New Composition Theorem for Learning Algorithms (NHB), pp. 583–589.
- ICALP-1998-Lugiez #automaton #induction #proving #theorem proving
- A Good Class of Tree Automata and Application to Inductive Theorem Proving (DL), pp. 409–420.
- ICALP-1998-Mellies #on the #theorem
- On a Duality Between Kruskal and Dershowitz Theorems (PAM), pp. 518–529.
- ALP-PLILP-1998-GoguenMK #theorem
- A Hidden Herbrand Theorem (JAG, GM, TK), pp. 445–462.
- CADE-1998-BenzmullerK98a #higher-order #proving #theorem proving
- System Description: LEO — A Higher-Order Theorem Prover (CB, MK), pp. 139–144.
- CADE-1998-FeveW #algebra #geometry #proving #theorem #using
- Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules (SF, DW), pp. 17–31.
- CADE-1998-FleuriotP #analysis #geometry #proving #standard #theorem proving
- A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia (JDF, LCP), pp. 3–16.
- CADE-1998-GorePSV #proving #smarttech #theorem proving
- System Description: card TAP: The First Theorem Prover on a Smart Card (RG, JP, AS, HV), pp. 47–50.
- CADE-1998-SchurmannP #automation #logic #proving #theorem proving
- Automated Theorem Proving in a Simple Meta-Logic for LF (CS, FP), pp. 286–300.
- CAV-1998-Camilleri #design #multi #proving #theorem proving
- A Role for Theorem Proving in Multi-Processor Design (AJC), pp. 45–48.
- CAV-1998-HardinWG #concept #design #proving #theorem proving
- Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle (DSH, MW, DAG), pp. 39–44.
- CSL-1998-Hajek #fuzzy #logic #theorem
- Trakhtenbrot Theorem and Fuzzy Logic (PH), pp. 1–8.
- CSL-1998-KomaraV #programming #theorem
- Theorems af Péter and Parsons in Computer Programming (JK, PJV), pp. 204–223.
- LICS-1998-Bernstein #congruence #higher-order #semantics #theorem
- A Congruence Theorem for Structured Operational Semantics of Higher-Order Languages (KLB), pp. 153–164.
- LICS-1998-Mellies #theorem
- A Stability Theorem in Rewriting Theory (PAM), pp. 287–298.
- LICS-1998-Voronkov #automation #reasoning #semantics #theorem
- Herbrand’s Theorem, Automated Reasoning and Semantics Tableaux (AV), pp. 252–263.
- RTA-1998-Ohlebusch #equivalence #reduction #theorem
- Church-Rosser Theorems for Abstract Reduction Modulo an Equivalence Relation (EO), pp. 17–31.
- TACAS-1997-SandnerM #proving #refinement #theorem proving
- Theorem Prover Support for the Refinement of Stream Processing Functions (RS, OM), pp. 351–365.
- STOC-1997-Ben-DavidBK #algorithm #composition #concept #geometry #learning #theorem
- A Composition Theorem for Learning Algorithms with Applications to Geometric Concept Classes (SBD, NHB, EK), pp. 324–333.
- ICALP-1997-Roura #divide and conquer #theorem
- An Improved Master Theorem for Divide-and-Conquer Recurrences (SR), pp. 449–459.
- FME-1997-AgerholmF #automation #proving #theorem proving #towards
- Towards an Integrated CASE and Theorem Proving Tool for VDM-SL (SA, JF), pp. 278–297.
- CADE-1997-Bonacina #proving #theorem proving
- The Clause-Diffusion Theorem Prover Peers-mcd (System Description) (MPB), pp. 53–56.
- CADE-1997-DahnGHW #automation #integration #interactive #proving #theorem proving
- Integration of Automated and Interactive Theorem Proving in ILP (BID, JG, TH, AW), pp. 57–60.
- CADE-1997-FeltyH #hybrid #interactive #proving #theorem proving #using
- Hybrid Interactive Theorem Proving Using Nuprl and HOL (APF, DJH), pp. 351–365.
- CADE-1997-HasegawaIOK #bottom-up #proving #set #theorem proving #top-down
- Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving (RH, KI, YO, MK), pp. 176–190.
- CADE-1997-Iwanuma #proving #theorem proving #top-down
- Lemma Matching for a PTTP-based Top-down Theorem Prover (KI), pp. 146–160.
- CADE-1997-LoweD #named #proving #theorem proving
- XBarnacle: Making Theorem Provers More Accessible (HL, DD), pp. 404–407.
- CADE-1997-Slaney #logic #named #proving #theorem proving
- Minlog: A Minimal Logic Theorem Prover (JKS), pp. 268–271.
- LICS-1997-AsarinCM #automaton #theorem
- A Kleene Theorem for Timed Automata (EA, PC, OM), pp. 160–171.
- LICS-1997-Janin #automaton #calculus #fixpoint #reduction #theorem
- Automata, Tableaus and a Reduction Theorem for Fixpoint Calculi in Arbitrary Complete Lattices (DJ), pp. 172–182.
- RTA-1997-KuhlerW #data type #equation #induction #proving #specification #theorem proving
- Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving (UK, CPW), pp. 38–52.
- TLCA-1997-Ruess #calculus #proving #theorem proving
- Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving (HR), pp. 319–335.
- ICALP-1996-Ganzinger #proving #theorem proving
- Saturation-Based Theorem Proving (Abstract) (HG), pp. 1–3.
- ICALP-1996-Lenzi #calculus #theorem #μ-calculus
- A Hierarchy Theorem for the μ-Calculus (GL), pp. 87–97.
- FME-1996-HavelundS #model checking #protocol #proving #theorem proving #verification
- Experiments in Theorem Proving and Model Checking for Protocol Verification (KH, NS), pp. 662–681.
- ICPR-1996-Chernov #theorem
- Tauber theorems for Dirichlet series and fractals (VMC), pp. 656–661.
- ICPR-1996-LinF #fourier #re-engineering #slicing #theorem #using
- Range data reconstruction using Fourier slice theorem (SSL, CSF), pp. 874–878.
- KR-1996-SiegelF #logic #representation #theorem
- A Representation Theorem for Preferential Logics (PS, LF), pp. 453–460.
- ALP-1996-Suzuki #revisited #standard #theorem
- Standardization Theorem Revisited (TS), pp. 122–134.
- CADE-1996-BeckertHOS #proving #theorem proving
- The Tableau-based Theorem Prover 3TAP Version 4.0 (BB, RH, PO, MS), pp. 303–307.
- CADE-1996-DenzingerS #learning #proving #theorem proving
- Learning Domain Knowledge to Improve Theorem Proving (JD, SS), pp. 62–76.
- CADE-1996-Ganzinger #proving #theorem proving
- Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract) (HG), p. 1.
- CADE-1996-GanzingerW #monad #proving #theorem proving
- Theorem Proving in Cancellative Abelian Monoids (Extended Abstract) (HG, UW), pp. 388–402.
- CADE-1996-KolbeW #proving #reuse #termination #theorem proving
- Termination of Theorem Proving by Reuse (TK, CW), pp. 106–120.
- CADE-1996-Luz-Filho #logic #proving #specification #theorem proving
- Grammar Specification in Categorial Logics and Theorem Proving (SFLF), pp. 703–717.
- CADE-1996-Martin #proving #theorem proving
- Theorem Proving with Group Presentations: Examples and Questions (UM), pp. 358–372.
- CADE-1996-MelisW #proving #theorem proving
- Internal Analogy in Theorem Proving (EM, JW), pp. 92–105.
- CADE-1996-SchaubBN #named #prolog #proving #reasoning #theorem proving
- XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description (TS, SB, PN), pp. 293–297.
- CADE-1996-Schumann #named #parallel #proving #theorem proving
- SiCoTHEO: Simple Competitive Parallel Theorem Provers (JS), pp. 240–244.
- CADE-1996-Tammet #logic #proving #theorem proving
- A Resolution Theorem Prover for Intuitonistic Logic (TT), pp. 2–16.
- CADE-1996-Wang #geometry #named #proving #theorem proving
- GEOTHER: A Geometry Theorem Prover (DW), pp. 166–170.
- CAV-1996-ClarkeGZ #algorithm #proving #theorem proving #using #verification
- Verifying the SRT Division Algorithm Using Theorem Proving Techniques (EMC, SMG, XZ), pp. 111–122.
- CAV-1996-GrafS #invariant #proving #theorem proving #using #verification
- Verifying Invariants Using theorem Proving (SG, HS), pp. 196–207.
- CAV-1996-Gribomont #reduction #refinement #theorem
- Atomicity Refinement and Trace Reduction Theorems (EPG), pp. 311–322.
- JICSLP-1996-AravindanBDFNNSS #logic programming #on the #paradigm #proving #theorem proving
- On Merging Theorem Proving and Logic Programming Paradigms (Poster Abstract) (CA, PB, JD, UF, GN, IN, DS, FS), p. 546.
- LICS-1996-AbdullaCJT #decidability #infinity #theorem
- General Decidability Theorems for Infinite-State Systems (PAA, KC, BJ, YKT), pp. 313–321.
- LICS-1996-MedinaI #theorem
- A Generalization of Fagin’s Theorem (JAM, NI), pp. 2–12.
- RTA-1996-BoudetCM #proving #theorem proving #unification
- AC-Complete Unification and its Application to Theorem Proving (AB, EC, CM), pp. 18–32.
- RTA-1996-HillenbrandBF #on the #performance #proving #theorem proving
- On Gaining Efficiency in Completion-Based Theorem Proving (TH, AB, RF), pp. 432–435.
- RTA-1996-Luth #algebra #composition #proving #term rewriting #theorem
- Compositional Term Rewriting: An Algebraic Proof of Toyama’s Theorem (CL), pp. 261–275.
- RTA-1996-Stuber #integer #proving #theorem proving
- Superposition Theorem Proving for Albelian Groups Represented as Integer Modules (JS), pp. 33–47.
- STOC-1995-GalilY #theorem
- Short length versions of Menger’s theorem (Extended Abstract) (ZG, XY), pp. 499–508.
- STOC-1995-Raz #parallel #theorem
- A parallel repetition theorem (RR), pp. 447–456.
- CAV-1995-DingelF #abstraction #infinity #model checking #proving #reasoning #theorem proving #using
- Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving (JD, TF), pp. 54–69.
- ICLP-1995-FormicaMT #database #object-oriented #proving #satisfiability #theorem proving
- A Theorem Prover for Checking Satisfiability of Object-Oriented Database Schemas (AF, MM, RT), p. 819.
- ICLP-1995-Hasegawa #generative #proving #theorem proving
- Model Generation Theorem Provers and Their Applications (RH), p. 7.
- RTA-1995-Holmes #equation #proving #recursion #theorem
- Disguising Recursively Chained Rewrite Rules as Equational Theorems, as Implemented in the Prover EFTTP Mark 2 (MRH), pp. 432–437.
- RTA-1995-Stickel #proving #term rewriting #theorem proving
- Term Rewriting in Contemporary Resolution Theorem Proving (Abstract) (MES), p. 101.
- STOC-1994-HerlihyS #theorem
- A simple constructive computability theorem for wait-free computation (MH, NS), pp. 243–252.
- STOC-1994-RajagopalanS #distributed #theorem
- A coding theorem for distributed computation (SR, LJS), pp. 790–799.
- ICALP-1994-Droste #concurrent #monad #theorem
- A KLeene Theorem for Recognizable Languages over Concurrency Monoids (MD), pp. 388–399.
- ALP-1994-BidoitH #behaviour #first-order #logic #proving #standard #theorem
- Proving Behavioural Theorems with Standard First-Order Logic (MB, RH), pp. 41–58.
- CADE-1994-BeckertP #agile #named #proving #theorem proving
- leanTAP: Lean Tableau-Based Theorem Proving (Extended Abstract) (BB, JP), pp. 793–797.
- CADE-1994-BonacinaM #distributed #proving #theorem proving
- Distributed Theorem Proving by Peers (MPB, WM), pp. 841–845.
- CADE-1994-ChuP #first-order #proving #semantics #theorem proving #using
- Semantically Guided First-Order Theorem Proving using Hyper-Linking (HC, DAP), pp. 192–206.
- CADE-1994-ClarkeZ #problem #proving #symbolic computation #theorem proving
- Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan (EMC, XZ), pp. 758–763.
- CADE-1994-FeltyH #proving #theorem proving
- Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables (APF, DJH), pp. 605–619.
- CADE-1994-McPheeCG #geometry #proving #theorem #using
- Mechanically Proving Geometry Theorems Using a Combination of Wu’s Method and Collins’ Method (NFM, SCC, XSG), pp. 401–415.
- CADE-1994-Plaisted #performance #proving #theorem proving
- The Search Efficiency of Theorem Proving Strategies (DAP), pp. 57–71.
- CADE-1994-Schumann #bottom-up #named #preprocessor #proving #theorem proving #top-down
- DELTA — A Bottom-up Preprocessor for Top-Down Theorem Provers — System Abstract (JS), pp. 774–777.
- CADE-1994-WaalG #logic programming #program analysis #program transformation #proving #theorem proving
- The Applicability of Logic Program Analysis and Transformation to Theorem Proving (DAdW, JPG), pp. 207–221.
- DAC-1993-JoyceS #evaluation #interactive #symbolic computation
- Linking BDD-Based Symbolic Evaluation to Interactive Theorem-Proving (JJJ, CJHS), pp. 469–474.
- STOC-1993-GargVY #approximate #multi #theorem
- Approximate max-flow min-(multi)cut theorems and their applications (NG, VVV, MY), pp. 698–707.
- STOC-1993-HerlihyS #theorem
- The asynchronous computability theorem for t-resilient tasks (MH, NS), pp. 111–120.
- ICALP-1993-MichauxV #automaton #theorem
- Cobham’s Ttheorem seen through Büchi’s Theorem (CM, RV), pp. 325–334.
- ICALP-1993-Senizergues #effectiveness #theorem
- An Effective Version of Stallings’ Theorem in the Case of Context-Free Groups (GS), pp. 478–495.
- CAV-1993-Hungar #model checking #parallel #process #proving #theorem proving #verification
- Combining Model Checking and Theorem Proving to Verify Parallel Processes (HH), pp. 154–165.
- ICLP-1993-Turner #logic programming #source code #theorem
- A Monotonicity Theorem for Extended Logic Programs (HT), pp. 567–585.
- RTA-1993-AvenhausD #equation #proving #theorem proving
- Distributing Equational Theorem Proving (JA, JD), pp. 62–76.
- RTA-1993-Bachmair #proving #theorem proving
- Rewrite Techniques in Theorem Proving (Abstract) (LB), p. 1.
- TLCA-1993-Groote #revisited #theorem
- The Conservation Theorem revisited (PdG), pp. 163–178.
- ESOP-1992-Gnaedig #proving #specification #theorem proving
- ELIOS-OBJ Theorem Proving in a Specification Language (IG), pp. 182–199.
- KR-1992-Lamarre #proving #theorem proving
- A Promenade from Monotonicity to Non-Monotonicity Following a Theorem Prover (PL), pp. 572–580.
- ALP-1992-BachmairGW #first-order #proving #theorem proving
- Theorem Proving for Hierarchic First-Order Theories (LB, HG, UW), pp. 420–434.
- CC-1992-KnoopS #interprocedural #theorem
- The Interprocedural Coincidence Theorem (JK, BS), pp. 125–140.
- CADE-1992-AlexanderP #proving #similarity #theorem
- Proving Equality Theorems with Hyper-Linking (GDA, DAP), pp. 706–710.
- CADE-1992-AstrachanS #proving #theorem proving
- Caching and Lemmaizing in Model Elimination Theorem Provers (OLA, MES), pp. 224–238.
- CADE-1992-Baker-PlummerR #proving #theorem proving
- The GAZER Theorem Prover (DBP, AR), pp. 726–730.
- CADE-1992-BeckertGHK #logic #multi #proving #theorem proving
- The Tableau-Based Theorem Prover 3TAP for Multi-Valued Logics (BB, SG, RH, WK), pp. 758–760.
- CADE-1992-Chen #empirical #knowledge-based #proving #theorem proving
- Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic (WZC), pp. 552–566.
- CADE-1992-Chou #geometry #proving #theorem proving
- A Geometry Theorem Prover for Macintoshes (SCC), pp. 686–690.
- CADE-1992-ClarkeZ #named #proving #theorem proving
- Analytica — A Theorem Prover in Mathematica (EMC, XZ), pp. 761–765.
- CADE-1992-Dafa #automation #deduction #proving #theorem proving
- A Natural Deduction Automated Theorem Proving System (LD), pp. 668–672.
- CADE-1992-HasegawaKF #generative #lazy evaluation #named #parallel #proving #theorem proving
- MGTP: A Parallel Theorem Prover Based on Lazy Model Generation (RH, MK, HF), pp. 776–780.
- CADE-1992-InoueKH #generative #proving #theorem proving
- Embedding Negation as Failure into a Model Generation Theorem Prover (KI, MK, RH), pp. 400–415.
- CADE-1992-LuskMS #named #parallel #proving #theorem proving
- ROO: A Parallel Theorem Prover (ELL, WM, JKS), pp. 731–734.
- CADE-1992-NieuwenhuisR #proving #theorem proving
- Theorem Proving with Ordering Constrained Clauses (RN, AR), pp. 477–491.
- CADE-1992-RandellCC #automation #challenge #proving #theorem proving
- Computing Transivity Tables: A Challenge For Automated Theorem Provers (DAR, AGC, ZC), pp. 786–790.
- CADE-1992-Schumann #logic #named #proving #theorem proving
- KPROP — An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract) (JS), pp. 740–742.
- CADE-1992-Voronkov #logic #proving #standard #theorem proving
- Theorem Proving in Non-Standard Logics Based on the Inverse Method (AV), pp. 648–662.
- CADE-1992-ZhangH #induction #proving #set #theorem
- Proving the Chinese Remainder Theorem by the Cover Set Induction (HZ, XH), pp. 431–445.
- CAV-1992-WrightL #algorithm #concurrent #proving #reasoning #theorem proving #using
- Using a Theorem Prover for Reasoning about Concurrent Algorithms (JvW, TL), pp. 56–68.
- LICS-1992-GonthierLM #standard #theorem
- An abstract standardisation theorem (GG, JJL, PAM), pp. 72–81.
- STOC-1991-Kilian #game studies #theorem
- A General Completeness Theorem for Two-Party Games (JK), pp. 553–560.
- ICALP-1991-GastinPZ #infinity #theorem
- A Kleene Theorem for Infinite Trace Languages (PG, AP, WZ), pp. 254–266.
- ICALP-1991-Wilke #theorem
- An Eilenberg Theorem for Infinity-Languages (TW), pp. 588–599.
- KR-1991-HalpernV #model checking #proving #theorem proving
- Model Checking vs. Theorem Proving: A Manifesto (JYH, MYV), pp. 325–334.
- PLILP-1991-FrausH #proving #theorem proving
- A Narrowing-Based Theorem Prover (UF, HH), pp. 421–422.
- ICLP-1991-FujitaH #algorithm #generative #proving #theorem proving #using
- A Model Generation Theorem Prover in KL1 Using a Ramified -Stack Algorithm (HF, RH), pp. 535–548.
- ICLP-1991-Hagiya #higher-order #proving #theorem proving #unification
- Higher-Order Unification as a Theorem Proving Procedure (MH), pp. 270–284.
- LICS-1991-Kozen #algebra #theorem
- A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events (DK), pp. 214–225.
- RTA-1991-Avenhaus #equation #induction #proving #theorem
- Proving Equational and Inductive Theorems by Completion and Embedding Techniques (JA), pp. 361–373.
- RTA-1991-BonacinaH #on the #proving #theorem proving
- On Fairness of Completion-Based Theorem Proving Strategies (MPB, JH), pp. 348–360.
- RTA-1991-Deruyver #equation #first-order #logic #named #proving #theorem proving
- EMMY: A Refutational Theorem Prover for First-Order Logic with Equation (AD), pp. 439–441.
- RTA-1991-Fraus #proving #theorem proving
- A Narrowing-Based Theorem Prover (UF), pp. 435–436.
- STOC-1990-AlonST #graph #theorem
- A Separator Theorem for Graphs with an Excluded Minor and its Applications (NA, PDS, RT), pp. 293–299.
- STOC-1990-KirkpatrickMY #multi #theorem
- Quantitative Steinitz’s Theorems with Applications to Multifingered Grasping (DGK, BM, CKY), pp. 341–351.
- POPL-1990-HeintzeJ #approximate #finite #logic programming #source code #theorem
- A Finite Presentation Theorem for Approximating Logic Programs (NH, JJ), pp. 197–209.
- ICSE-1990-LafontaineLS #case study #development #empirical #formal method #proving #theorem proving #using
- An Experiment in Formal Software Development: Using the B Theorem Prover on a VDM Case Study (CL, YL, PYS), pp. 34–42.
- CADE-1990-AndrewsINP #proving #theorem proving
- The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 641–642.
- CADE-1990-BoyerM #logic #proving #theorem proving
- A Theorem Prover for a Computational Logic (RSB, JSM), pp. 1–15.
- CADE-1990-ButlerFJO #parallel #proving #theorem proving
- A High-Performance Parallel Theorem Prover (RB, ITF, AJ, RAO), pp. 649–650.
- CADE-1990-ChouG #algorithm #composition #geometry #proving #theorem proving
- Ritt-Wu’s Decomposition Algorithm and Geometry Theorem Proving (SCC, XSG), pp. 207–220.
- CADE-1990-CostaHLS #automation #implementation #logic #proving #theorem proving
- Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation (NCAdC, LJH, JJL, VSS), pp. 72–86.
- CADE-1990-Gramlich #induction #named #proving #theorem proving
- UNICOM: A Refined Completion Based Inductive Theorem Prover (BG), pp. 655–656.
- CADE-1990-HeiselRS #proving #theorem proving #verification
- Tactical Theorem Proving in Program Verification (MH, WR, WS), pp. 117–131.
- CADE-1990-HsiangJ #proving #theorem proving #tutorial
- Tutorial on Rewrite-Based Theorem Proving (JH, JPJ), p. 684.
- CADE-1990-KaflZ #proving #theorem proving #verification
- The Theorem Prover of the Program Verifier Tatzelwurm (TK, NZ), pp. 657–658.
- CADE-1990-LuskM #automation #proving #theorem proving #tutorial
- Tutorial on High-Performance Automated Theorem Proving (ELL, WM), p. 681.
- CADE-1990-MurrayR #named #proving #theorem proving
- DISSOLVER: A Dissolution-based Theorem Prover (NVM, ER), pp. 665–666.
- CADE-1990-SchumannL #named #parallel #proving #theorem proving
- PARTHEO: A High-Performance Parallel Theorem Prover (JS, RL), pp. 40–56.
- CADE-1990-SchumannLK #implementation #parallel #performance #proving #theorem proving #tutorial
- Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation (JS, RL, FJK), p. 683.
- CADE-1990-Schwind #decidability #logic #proving #set #theorem proving
- A Tableau-Based Theorem Prover for a Decidable Subset of Default Logic (CS), pp. 528–542.
- CADE-1990-Stickel #prolog #proving #theorem proving
- A Prolog Technology Theorem Prover (MES), pp. 673–674.
- CADE-1990-Sutcliffe #proving #theorem proving
- A General Clause Theorem Prover (GS), pp. 675–676.
- CADE-1990-Tarver #prolog
- An Examination of the Prolog Technology Theorem-Prover (MT), pp. 322–335.
- CADE-1990-Tuominen #framework #logic #proving #theorem proving
- Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic (HT), pp. 514–527.
- CSL-1990-Pudlak #bound #theorem
- Ramsey’s Theorem in Bounded Arithmetic (PP), pp. 308–317.
- PODS-1989-RamakrishnanSUV #theorem
- Proof-Tree Transformation Theorems and Their Applications (RR, YS, JDU, MYV), pp. 172–181.
- FPCA-1989-Wadler #exclamation #for free #theorem
- Theorems for Free! (PW), pp. 347–359.
- CSL-1989-PasztorS #theorem
- A Streamlined Temporal Completeness Theorem (AP, IS), pp. 322–336.
- LICS-1989-BoseCLM #horn clause #named #parallel #proving #theorem proving
- PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (SB, EMC, DEL, SM), pp. 80–89.
- RTA-1989-AvenhausDM #named #performance #proving #theorem proving
- THEOPOGLES — An efficient Theorem Prover based on Rewrite-Techniques (JA, JD, JM), pp. 538–541.
- RTA-1989-BonacinaS #equation #named #proving #theorem proving
- KBlab: An Equational Theorem Prover for the Macintosh (MPB, GS), pp. 548–550.
- SIGMOD-1988-MazumdarSS #proving #security #theorem proving #using
- Resolving the Tension between Integrity and Security Using a Theorem Prover (SM, DWS, TS), pp. 233–242.
- STOC-1988-Ben-OrGW #distributed #fault tolerance #theorem
- Completeness Theorems for Non-Cryptographic Fault-Tolerant Distributed Computation (Extended Abstract) (MBO, SG, AW), pp. 1–10.
- ICALP-1988-MehlhornY #how #theorem
- Constructive Hopf’s Theorem: Or How to Untangle Closed Planar Curves (KM, CKY), pp. 410–423.
- VDME-1988-JonesM #design #empirical #named #proving #theorem proving #user interface
- MUFFIN: A User Interface Design Experiment for a Theorem Proving Assistant (CBJ, RCM), pp. 337–375.
- ALP-1988-HofbauerK #induction #proving #term rewriting #theorem
- Proving Inductive Theorems Based on Term Rewriting Systems (DH, RDK), pp. 180–190.
- CADE-1988-AllenBCM #horn clause #named #parallel #proving #theorem proving
- PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (PEA, SB, EMC, SM), pp. 764–765.
- CADE-1988-AndrewsINP #proving #theorem proving
- The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 760–761.
- CADE-1988-BrownP #logic #named #proving #theorem proving
- SYMEVAL: A Theorem Prover Based on the Experimental Logic (FMB, SSP), pp. 756–757.
- CADE-1988-CyrlukHK #algebra #geometry #named #proving #theorem proving
- GEOMETER: A Theorem Prover for Algebraic Geometry (DC, RMH, DK), pp. 770–771.
- CADE-1988-FeltyM #higher-order #logic programming #programming language #proving #specification #theorem proving
- Specifying Theorem Provers in a Higher-Order Logic Programming Language (APF, DM), pp. 61–80.
- CADE-1988-Hines #knowledge-based #proving #theorem proving
- Hyper-Chaining and Knowledge-Based Theorem Proving (LMH), pp. 469–486.
- CADE-1988-Kaufmann #interactive #proving #theorem proving
- An Interactive Enhancement to the Boyer-Moore Theorem Prover (MK), pp. 735–736.
- CADE-1988-MantheyB #named #prolog #proving #theorem proving
- SATCHMO: A Theorem Prover Implemented in Prolog (RM, FB), pp. 415–434.
- CADE-1988-McRobbieMT #automation #knowledge-based #logic #performance #proving #standard #theorem proving #towards
- Towards Efficient “Knowledge-Based” Automated Theorem Proving for Non-Standard Logics (MAM, RKM, PBT), pp. 197–217.
- CADE-1988-Paulson #named #proving #theorem proving
- Isabelle: The Next Seven Hundred Theorem Provers (LCP), pp. 772–773.
- CADE-1988-Plaisted #proving #theorem proving
- A Goal Directed Theorem Prover (DAP), p. 737.
- CADE-1988-Stevens #challenge #problem #proving #theorem proving
- Challenge Problems from Nonassociative Rings for Theorem Provers (RLS), pp. 730–734.
- CADE-1988-Stickel88a #prolog #proving #theorem proving
- A Prolog Technology Theorem Prover (MES), pp. 752–753.
- CADE-1988-WosM #automation #challenge #combinator #logic #problem #similarity #source code
- Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs (LW, WM), pp. 714–729.
- CADE-1988-ZhangK #first-order #proving #theorem proving #using
- First-Order Theorem Proving Using Conditional Rewrite Rules (HZ, DK), pp. 1–20.
- STOC-1987-GoldreichMW #game studies #how #protocol #theorem
- How to Play any Mental Game or A Completeness Theorem for Protocols with Honest Majority (OG, SM, AW), pp. 218–229.
- ICALP-1987-Kuich #theorem
- The Kleene and the Parikh Theorem in Complete Semirings (WK), pp. 212–225.
- LICS-1987-BachmairD #first-order #proving #theorem proving
- Inference Rules for Rewrite-Based First-Order Theorem Proving (LB, ND), pp. 331–337.
- LICS-1987-GallierRS #equation #proving #theorem proving #using
- Theorem Proving Using Rigid E-Unification Equational Matings (JHG, SR, WS), pp. 338–346.
- ICALP-1986-Regan #reduction #theorem
- A Uniform Reduction Theorem — Extending a Result of J. Grollmann and A. Selman (KWR), pp. 324–333.
- POPL-1986-LengauerH #concurrent #network #sorting #theorem
- A Mechanically Certified Theorem about Optimal Concurrency of Sorting Networks (CL, CHH), pp. 307–317.
- CADE-1986-AbadiM #proving #theorem proving
- Modal Theorem Proving (MA, ZM), pp. 172–189.
- CADE-1986-AndrewsPIK #proving #theorem proving
- The TPS Theorem Proving System (PBA, FP, SI, CPK), pp. 663–664.
- CADE-1986-BeierleOV #automation #proving #theorem proving
- Automatic Theorem Proving in the ISDV System (CB, WGO, AV), pp. 670–671.
- CADE-1986-BiundoHHW #induction #proving #theorem proving
- The Karlsruhe Induction Theorem Proving System (SB, BH, DH, CW), pp. 672–674.
- CADE-1986-BoyerM #bibliography #logic
- Overview of a Theorem-Prover for A Computational Logic (RSB, JSM), pp. 675–678.
- CADE-1986-ButlerLMO #automation #proving #theorem proving
- Paths to High-Performance Automated Theorem Proving (RB, ELL, WM, RAO), pp. 588–597.
- CADE-1986-Chou #geometry #named #proving #theorem proving
- GEO-Prover — A Geometry Theorem Prover Developed at UT (SCC), pp. 679–680.
- CADE-1986-GreenbaumP #proving #theorem proving
- The Illinois Prover: A General Purpose Resolution Theorem Prover (SG, DAP), pp. 685–687.
- CADE-1986-HsiangR #proving #theorem proving
- A New Method for Establishing Refutational Completeness in Theorem Proving (JH, MR), pp. 141–152.
- CADE-1986-Huet86a #proving #theorem proving
- Theorem Proving Systems of the Formel Project (GPH), pp. 687–688.
- CADE-1986-KutzlerS #algorithm #geometry #proving #theorem proving
- A Geometry Theorem Prover Based on Buchberger’s Algorithm (BK, SS), pp. 693–694.
- CADE-1986-LoganantharajM #graph #parallel #proving #theorem proving
- Parallel Theorem Proving with Connection Graphs (RL, RAM), pp. 337–352.
- CADE-1986-Stickel #compilation #implementation #prolog #proving #theorem proving
- A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler (MES), pp. 573–587.
- CADE-1986-ThistlewaiteMM #automation #proving #theorem proving
- The KRIPKE Automated Theorem Proving System (PBT, MAM, RKM), pp. 705–706.
- LICS-1986-ChouK #geometry #on the #proving #theorem proving
- On Mechanical Theorem Proving in Minkowskian Plane Geometry (SCC, HPK), pp. 187–192.
- ICALP-1985-Coppo #recursion #theorem
- A Completeness Theorem for Recursively Defined Types (MC), pp. 120–129.
- ICALP-1985-Hansel #proving #theorem
- A Simple Proof of the Skolem-Mahler-Lech Theorem (GH), pp. 244–249.
- ICALP-1985-Hortala-GonzalezR #hoare #logic #nondeterminism #source code #standard #theorem
- Hoare’s Logic for Nondeterministic Regular Programs: A Nonstandard Completeness Theorem (MTHG, MRA), pp. 270–280.
- RTA-1985-Hsiang #proving #term rewriting #theorem proving
- Two Results in Term Rewriting Theorem Proving (JH), pp. 301–324.
- STOC-1984-AjtaiB #constant #probability #theorem
- A Theorem on Probabilistic Constant Depth Computations (MA, MBO), pp. 471–474.
- CADE-1984-OhlbachW #automation #logic #problem #proving #theorem proving
- Solving a Problem in Relevance Logic with an Automated Theorem Prover (HJO, GW), pp. 496–508.
- CADE-1984-Plaisted #analysis #dependence #graph #proving #theorem proving #using
- Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving (DAP), pp. 356–374.
- CADE-1984-Stickel #case study #commutative #proving #theorem proving
- A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity (MES), pp. 248–258.
- CADE-1984-Suppes #generative #interactive #proving #theorem proving
- The Next Generation of Interactive Theorem Provers (PS), pp. 303–315.
- SLP-1984-Stickel84 #prolog #proving #theorem proving
- A Prolog Technology Theorem Prover (MES), pp. 211–217.
- ICALP-1983-HsiangD #proving #theorem proving
- Rewrite Methods for Clausal and Non-Clausal Theorem Proving (JH, ND), pp. 331–346.
- ICALP-1982-Brandenburg #theorem
- Extended Chomsky-Schützenberger Theorems (FJB), pp. 83–93.
- ICALP-1982-KrevnerY #precedence #theorem
- An Iteration Theorem for Simple Precedence Languages (Extended Abstract) (YK, AY), pp. 360–368.
- CADE-1982-Wos #automation
- Solving Open Questions with an Automated Theorem-Proving Program (LW), pp. 1–31.
- STOC-1981-Leivant #complexity #independence #parametricity #polymorphism #programming language #theorem
- 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 #theorem
- A Representation Theorem for Models of *-Free PDL (DK), pp. 351–362.
- ICALP-1980-Turchin #optimisation #proving #theorem proving
- The Use of Metasystem Transition in Theorem Proving and Program Optimization (VFT), pp. 645–657.
- CADE-1980-EricksonM #proving #scalability #theorem proving
- The AFFIRM Theorem Prover: Proof Forests and Management of Large Proofs (RWE, DRM), pp. 220–231.
- CADE-1980-Gloess #correctness #empirical #parsing #proving #theorem proving
- An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions (PYG), pp. 154–169.
- CADE-1980-Nederpelt #approach #proving #theorem proving #λ-calculus
- An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus (RN), pp. 182–194.
- CADE-1980-OverbeekL #architecture #data type #implementation #source code
- Data Structures and Control Architectures for Implementation of Theorem-Proving Programs (RAO, ELL), pp. 232–249.
- CADE-1980-Plaisted #abstraction #proving #theorem proving
- Abstraction Mappings in Mechanical Theorem Proving (DAP), pp. 264–280.
- STOC-1979-ODonnell #independence #programming language #theorem
- A Programming Language Theorem Which Is Independent of Peano Arithmetic (MO), pp. 176–188.
- ICALP-1979-Istrail #fixpoint #monad #recursion #semantics #source code #theorem
- 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 #theorem
- A Unique Termination Theorem for a Theory with Generalised Commutative Axioms (HJJ), pp. 316–330.
- STOC-1977-Beatty #ll #theorem
- Iteration Theorems for LL(k) Languages (JCB), pp. 122–131.
- POPL-1977-DeMilloLP #process #proving #social #source code #theorem
- Social Processes and Proofs of Theorems and Programs (RAD, RJL, AJP), pp. 206–214.
- ICALP-1976-Galil #integer #on the #programming #proving #theorem proving
- On Enumeration Procedures for Theorem Proving and for Integer Programming (ZG), pp. 355–381.
- STOC-1975-Perrault #theorem #transducer
- Intercalation Theorems for Tree Transducer Languages (CRP), pp. 126–136.
- ICALP-1974-Leeuwen #formal method #theorem
- A Generalisation of Parikh’s Theorem in Formal Language Theory (JvL), pp. 17–26.
- ICALP-1972-Vilfan #theorem
- A Generalization of a Theorem of Specker and Some Applications (BV), pp. 609–622.
- STOC-1971-Boasson #theorem
- An Iteration Theorem for One-Counter Languages (LB), pp. 116–120.
- STOC-1971-Cook #complexity
- The Complexity of Theorem-Proving Procedures (SAC), pp. 151–158.
- STOC-1970-KingF #integer #proving #theorem proving
- An Interpretation Oriented Theorem Prover over Integers (JCK, RWF), pp. 169–179.
- STOC-1970-Reiter #proving #theorem proving
- The Predicate Elimination Strategy in Theorem Proving (RR), pp. 180–183.
- STOC-1970-Rosen #theorem
- Tree-Manipulating Systems and Church-Rosser Theorems (BKR), pp. 117–127.
- STOC-1970-Rounds #proving #theorem
- Tree-Oriented Proofs of Some Theorems on Context-Free and Indexed Languages (WCR), pp. 109–116.
- STOC-1970-Ullian #product line #theorem
- Three Theorems on Abstract Families of Languages (JSU), pp. 226–230.
- STOC-1969-Ogden #stack #theorem
- Intercalation Theorems for Stack Languages (WFO), pp. 31–42.