BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Used together with:
prove (168)
prover (125)
logic (51)
base (40)
use (39)

Stem theorem$ (all stems)

515 papers:

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

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.