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.