BibSLEIGH — theorem proving tag

theorem proving

theorem proving

Tag #theorem proving

404 papers:

IFM-2019-KringsL #constraints #interactive #proving: Embedding SMT-LIB into B for Interactive Proof and Constraint Solving (SK, ML), pp. 265–283.
Haskell-2019-HallahanXP #constraints #haskell #named: G2Q: Haskell constraint solving (WTH, AX, RP), pp. 44–57.
ICML-2019-BansalLRSW #higher-order #logic #machine learning #named #proving: HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving (KB, SML, MNR, CS, SW), pp. 454–463.
PADL-2019-Tarau #combinator #framework #proving #testing: A Combinatorial Testing Framework for Intuitionistic Propositional Theorem Provers (PT), pp. 115–132.
PPDP-2019-Kikuchi0S #induction #program transformation #proving #term rewriting: Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation (KK, TA0, IS), p. 14.
CADE-2019-LiT #automation #protocol #proving #security #verification: Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (DLL, AT), pp. 354–365.
SEFM-2018-DuboisGPC #interactive #protocol #proving #using: Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem Prover (CD, OG, JP, MC), pp. 239–253.
Haskell-2018-VazouBKHH #equation #functional #haskell #proving #reasoning: Theorem proving for all: equational reasoning in liquid Haskell (functional pearl) (NV, JB, RK, DVH, GH), pp. 132–144.
PPDP-2018-GreweEPM #automation #framework #proving: System Description: An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers (SG, SE, AP, MM), p. 10.
ICSME-2017-Shi #algorithm #constraints #optimisation: Combining Evolutionary Algorithms with Constraint Solving for Configuration Optimization (KS), pp. 665–669.
FDG-2017-KarthS #constraints: WaveFunctionCollapse is constraint solving in the wild (IK, AMS), p. 10.
ICSE-2017-ThomeSBB #constraints #detection #string: Search-driven string constraint solving for vulnerability detection (JT, LKS, DB, LCB), pp. 198–208.
CADE-2017-HustadtOD #logic #metric #proving: Theorem Proving for Metric Temporal Logic over the Naturals (UH, AO, CD), pp. 326–343.
CADE-2017-ItegulovSP #proving: Scavenger 0.1: A Theorem Prover Based on Conflict Resolution (DI, JS, BWP), pp. 344–356.
CADE-2017-MengRTB #constraints #relational #smt: Relational Constraint Solving in SMT (BM, AR, CT, CWB), pp. 148–165.
TAP-2017-Reger0V #case study #challenge #experience #proving #testing: Testing a Saturation-Based Theorem Prover: Experiences and Challenges (GR, MS0, AV), pp. 152–161.
ASE-2016-LiLQHBYCL #constraints #execution #machine learning #symbolic computation: Symbolic execution of complex program driven by machine learning based constraint solving (XL, YL, HQ, YQH, LB, YY, XC, XL), pp. 554–559.
ESOP-2016-MineBR #algorithm #constraints #induction #invariant #source code: An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs (AM, JB, TWR), pp. 560–588.
ICTSS-2016-PetrenkoNR #automaton #constraints #generative #testing: Test Generation by Constraint Solving and FSM Mutant Killing (AP, ONT, SR), pp. 36–51.
IJCAR-2016-BrombergerW #constraints #performance #testing: Fast Cube Tests for LIA Constraint Solving (MB, CW), pp. 116–132.
IJCAR-2016-SchulzM #heuristic #performance #proving: Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving (SS0, MM), pp. 330–345.
Haskell-2015-Gundry #constraints #haskell #plugin: A typechecker plugin for units of measure: domain-specific constraint solving in GHC Haskell (AG), pp. 11–22.
OOPSLA-2015-FelgentreffMBH #constraints #programming language: Checks and balances: constraint solving without surprises in object-constraint programming languages (TF, TDM, AB, RH), pp. 767–782.
ICSE-v1-2015-HenardPHT #configuration management #constraints #multi #product line #scalability: Combining Multi-Objective Search and Constraint Solving for Configuring Large Software Product Lines (CH, MP, MH, YLT), pp. 517–528.
ICSE-v1-2015-MilicevicNKJ #constraints #higher-order #relational: Alloy*: A General-Purpose Higher-Order Relational Constraint Solver (AM, JPN, EK, DJ), pp. 609–619.
CADE-2015-BackemanR #bound #proving: Theorem Proving with Bounded Rigid E-Unification (PB, PR), pp. 572–587.
CADE-2015-Baumgartner #named #proving: SMTtoTPTP — A Converter for Theorem Proving Formats (PB), pp. 285–294.
CADE-2015-BaumgartnerBW #named #proving: Beagle — A Hierarchic Superposition Theorem Prover (PB, JB, UW), pp. 367–377.
CADE-2015-FultonMQVP #axiom #hybrid #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: Automated Theorem Proving for Assertions in Separation Logic with All Connectives (ZH, RG, AT), pp. 501–516.
CADE-2015-MouraKADR #agile #proving: The Lean Theorem Prover (LMdM, SK, JA, FvD, JvR), pp. 378–388.
ISSTA-2015-KhoshnoodKW #concurrent #constraints #debugging #named: ConcBugAssist: constraint solving for diagnosis and repair of concurrency bugs (SK, MK, CW), pp. 165–176.
HOFM-2014-BeckertGB #evaluation #interactive #proving #usability #using: A Usability Evaluation of Interactive Theorem Provers Using Focus Groups (BB, SG, FB), pp. 3–19.
IFM-2014-BrideKP #constraints #specification #using #verification #workflow: Verifying Modal Workflow Specifications Using Constraint Solving (HB, OK, FP), pp. 171–186.
IFM-2014-ChaudhariD #automation #proving: Automated Theorem Prover Assisted Program Calculations (DLC, OPD), pp. 205–220.
SPLC-2014-ThumMBHRS #model checking #product line #proving: Potential synergies of theorem proving and model checking for software product lines (TT, JM, FB, MH, AvR, GS), pp. 177–186.
PADL-2014-CampeottoPDFP #constraints #using: Exploring the Use of GPUs in Constraint Solving (FC, ADP, AD, FF, EP), pp. 152–167.
ASE-2014-KauslerS #constraints #evaluation #execution #string #symbolic computation: Evaluation of string constraint solvers in the context of symbolic execution (SK, ES), pp. 259–270.
SAC-2014-AmadiniGM #constraints: An enhanced features extractor for a portfolio of constraint solvers (RA, MG, JM), pp. 1357–1359.
CAV-2014-Voronkov #architecture #first-order #named #proving: AVATAR: The Architecture for First-Order Theorem Provers (AV), pp. 696–710.
ICLP-J-2014-AmadiniGM #approach #constraints #lazy evaluation #named: SUNNY: a Lazy Portfolio Approach for Constraint Solving (RA, MG, JM), pp. 509–524.
IJCAR-2014-BaumgartnerBW #finite #proving #quantifier: Finite Quantification in Hierarchic Theorem Proving (PB, JB, UW), pp. 152–167.
IJCAR-2014-BeyersdorffC #complexity #proving: The Complexity of Theorem Proving in Circumscription and Minimal Entailment (OB, LC), pp. 403–417.
IJCAR-2014-GoreTW #logic #proving #using: A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description (RG, JT, JW), pp. 262–268.
TAP-2014-KurthSW #constraints #generative #interface #process #testing #uml #using: Generating Test Data from a UML Activity Using the AMPL Interface for Constraint Solvers (FK, SS, SW), pp. 169–186.
MoDELS-2013-SongBCC #adaptation #constraints #modelling #runtime #self #using: Self-adaptation with End-User Preferences: Using Run-Time Models and Constraint Solving (HS, SB, AC, SC), pp. 555–571.
POPL-2013-ParkSP #proving: A theorem prover for Boolean BI (JP, JS, SP), pp. 219–232.
DAC-2013-WuH #constraints #framework #multi #random #robust #set #verification: A robust constraint solving framework for multiple constraint sets in constrained random verification (BHW, CY(H), p. 7.
CADE-2013-HawblitzelKLR #automation #proving #source code #towards #using: Towards Modularly Comparing Programs Using Automated Theorem Provers (CH, MK, SKL, HR), pp. 282–299.
CAV-2013-KovacsV #first-order #proving: First-Order Theorem Proving and Vampire (LK, AV), pp. 1–35.
SAT-2013-Beyersdorff #complexity #logic #proving: The Complexity of Theorem Proving in Autoepistemic Logic (OB), pp. 365–376.
VMCAI-2013-PelleauMTB #abstract domain #constraints: A Constraint Solver Based on Abstract Domains (MP, AM, CT, FB), pp. 434–454.
ICSM-2012-RupakhetiH #constraints #fault #modelling #similarity #using: Finding errors from reverse-engineered equality models using a constraint solver (CRR, DH), pp. 77–86.
FM-2012-CarlierDG #constraints #finite: A Certified Constraint Solver over Finite Domains (MC, CD, AG), pp. 116–131.
FLOPS-2012-CastineirasS #constraints #performance: Improving the Performance of FD Constraint Solving in a CFLP System (IC, FSP), pp. 88–103.
FLOPS-2012-Triska #constraints #finite #prolog: The Finite Domain Constraint Solver of SWI-Prolog (MT), pp. 307–316.
ICFP-2012-StewartBA #proving: Verified heap theorem prover by paramodulation (GS, LB, AWA), pp. 3–14.
POPL-2012-Moore #proving: Meta-level features in an industrial-strength theorem prover (JSM), pp. 425–426.
ICSE-2012-BalasubramaniamJKMN #approach #automation #constraints #generative #performance: An automated approach to generating efficient constraint solvers (DB, CJ, LK, IM, PN), pp. 661–671.
ICSE-2012-SamirniSAMTH #automation #constraints #fault #generative #html #php #string #using: Automated repair of HTML generation errors in PHP applications using string constraint solving (HS, MS, SA, TDM, FT, LJH), pp. 277–287.
CAV-2012-BodikT #constraints #source code: Synthesizing Programs with Constraint Solvers (RB, ET), p. 3.
ICST-2012-SiddiquiMK #analysis #constraints #data flow #lightweight: Lightweight Data-Flow Analysis for Execution-Driven Constraint Solving (JHS, DM, SK), pp. 91–100.
ICST-2012-VorobyovK #automation #constraints #generative #static analysis #testing: Combining Static Analysis and Constraint Solving for Automatic Test Case Generation (KV, PK), pp. 915–920.
IJCAR-2012-JacquelBDD #automation #deduction #modulo theories #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-TraytelPB #category theory #composition #data type #higher-order #logic #proving: Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (DT, AP, JCB), pp. 596–605.
SAT-2012-ZhangMZ #constraints #identification #interactive #optimisation: Faulty Interaction Identification via Constraint Solving and Optimization (JZ, FM, ZZ), pp. 186–199.
WICSA-2011-BalasubramaniamSJKMN #approach #architecture #constraints #generative #named #performance: Dominion: An Architecture-Driven Approach to Generating Efficient Constraint Solvers (DB, LdS, CJ, LK, IM, PN), pp. 228–231.
SEFM-2011-ErnstSR #analysis #empirical #interactive #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 #using #verification: Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving (MJ, KB, DD, CD), pp. 253–268.
PLDI-2011-PerezR #calculus #logic #proving: Separation logic + superposition calculus = heap theorem prover (JANP, AR), pp. 556–566.
TACAS-2011-ChamarthiDMV #proving: The ACL2 Sedan Theorem Proving System (HRC, PCD, PM, DV), pp. 291–295.
CADE-2011-AspertiRCT #interactive #proving: The Matita Interactive Theorem Prover (AA, WR, CSC, ET), pp. 64–69.
CADE-2011-Brown #higher-order #problem #proving #satisfiability #sequence: 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 #using: Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving (MS, GS), pp. 461–475.
ICST-2011-KhalekK #constraints #database #relational #testing #using: Systematic Testing of Database Engines Using a Relational Constraint Solver (SAK, SK), pp. 50–59.
ICGT-2010-OrejasL #constraints #graph transformation: Delaying Constraint Solving in Symbolic Graph Transformation (FO, LL), pp. 43–58.
KEOD-2010-KatsumiG #lifecycle #ontology #proving: Theorem Proving in the Ontology Lifecycle (MK, MG), pp. 37–49.
SEKE-2010-FuL #constraints #detection #string #web: A String Constraint Solver for Detecting Web Application Vulnerability (XF, CCL), pp. 535–542.
ECMFA-2010-KleinerFA #automation #constraints #formal method #platform: Model Search: Formalizing and Automating Constraint Solving in MDE Platforms (MK, MDDF, PA), pp. 173–188.
PPDP-2010-Bonacina #on the #proving: On theorem proving for program checking: historical perspective and recent developments (MPB), pp. 1–12.
RE-2010-SalinesiMDD #constraints #integer #requirements #reuse #using: Using Integer Constraint Solving in Reuse Based Requirements Engineering (CS, RM, DD, OD), pp. 243–251.
ICSE-2010-Ma #analysis #constraints #testing: Constraint solving techniques for software testing and analysis (FM), pp. 417–420.
CAV-2010-Rybalchenko #constraints #theory and practice #verification: Constraint Solving for Program Verification: Theory and Practice by Example (AR), pp. 57–71.
CSL-2010-Rybalchenko #constraints #theory and practice #verification: Constraint Solving for Program Verification: Theory and Practice by Example (AR), p. 51.
ICTSS-2010-LakhotiaTHH #constraints #execution #float #named #search-based #symbolic computation: FloPSy — Search-Based Floating Point Constraint Solving for Symbolic Execution (KL, NT, MH, JdH), pp. 142–157.
IJCAR-2010-BaeldeMS #induction #proving: Focused Inductive Theorem Proving (DB, DM, ZS), pp. 278–292.
IJCAR-2010-KorovinS #named #proving #similarity: iProver-Eq: An Instantiation-Based Theorem Prover with Equality (KK, CS), pp. 196–202.
LICS-2010-Moore #proving #verification: Theorem Proving for Verification: The Early Days (JSM), p. 283.
TAP-2010-Rusu #proving #specification: Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications (VR), pp. 135–150.
ASE-2009-SiddiquiMK #constraints #optimisation #performance: Optimizing a Structural Constraint Solver for Efficient Software Checking (JHS, DM, SK), pp. 615–619.
SAC-2009-YangLLW #approach #approximate #constraints: An approximate approach to constraint solving in soft sensing (TY, ZL, XL, HW), pp. 1415–1416.
FASE-2009-KovacsV #array #invariant #proving #source code #using: Finding Loop Invariants for Programs over Arrays Using a Theorem Prover (LK, AV), pp. 470–485.
CADE-2009-BensaidCP #integer #named #proving: Dei: A Theorem Prover for Terms with Integer Exponents (HB, RC, NP), pp. 146–150.
CADE-2009-BonacinaLM #on the #proving #satisfiability: On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving (MPB, CL, LMdM), pp. 35–50.
CADE-2009-McLaughlinP #performance #proving: Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method (SM, FP), pp. 230–244.
CADE-2009-Stickel #proving: Building Theorem Provers (MES), pp. 306–321.
CADE-2009-SutcliffeBBT #automation #development #higher-order #logic #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: Termination Analysis by Dependency Pairs and Inductive Theorem Proving (SS, MP, JG, CF, PSK), pp. 322–338.
TestCom-FATES-2009-GrieskampQWKC #constraints #interactive #smt: Interaction Coverage Meets Path Coverage by SMT Constraint Solving (WG, XQ, XW, NK, MBC), pp. 97–112.
TestCom-FATES-2009-SubramaniamXGP #approach #proving #testing #using: An Approach for Test Selection for EFSMs Using a Theorem Prover (MS, LX, BG, ZP), pp. 146–162.
VMCAI-2009-TalyGT #constraints #logic #using: Synthesizing Switching Logic Using Constraint Solving (AT, SG, AT), pp. 305–319.
SEFM-2008-GuoS #finite #impact analysis #proving #state machine #using: Formal Change Impact Analyses of Extended Finite State Machines Using a Theorem Prover (BG, MS), pp. 335–344.
FLOPS-2008-MellarkodG #constraints #reasoning #set: Integrating Answer Set Reasoning with Constraint Solving Techniques (VSM, MG), pp. 15–31.
ICGT-2008-Pennemann #proving: Resolution-Like Theorem Proving for High-Level Conditions (KHP), pp. 289–304.
PADL-2008-Subbarayan #constraints #performance #reasoning: Efficient Reasoning for Nogoods in Constraint Solvers with BDDs (SS), pp. 53–67.
PLDI-2008-GulwaniSV #constraints #program analysis: Program analysis as constraint solving (SG, SS, RV), pp. 281–292.
ASE-2008-KhalekELK #constraints #generative #relational #testing #using: Query-Aware Test Generation Using a Relational Constraint Solver (SAK, BE, YOL, SK), pp. 238–247.
SAC-2008-AbedMS #analysis #graph #multi #proving #reachability #using: Reachability analysis using multiway decision graphs in the HOL theorem prover (SA, OAM, GAS), pp. 333–338.
GPCE-2008-ZhangAN #constraints #optimisation: From generic to specific: off-line optimization for a general constraint solver (YZ, TA, FN), pp. 45–54.
CAV-2008-Harrison #proving #verification: Theorem Proving for Verification (JH), pp. 11–18.
ICLP-2008-NearBF #declarative #first-order #logic #named #proving: αleanTAP: A Declarative Theorem Prover for First-Order Classical Logic (JPN, WEB, DPF), pp. 238–252.
ICLP-2008-Triska #constraints #finite: Generalising Constraint Solving over Finite Domains (MT), pp. 820–821.
IJCAR-2008-BenzmullerPTF #automation #higher-order #logic #named #proving: LEO-II — A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (CB, LCP, FT, AF), pp. 162–170.
IJCAR-2008-Gacek #interactive #proving: The Abella Interactive Theorem Prover (AG), pp. 154–161.
IJCAR-2008-Korovin #first-order #logic #named #proving: iProver — An Instantiation-Based Theorem Prover for First-Order Logic (KK), pp. 292–298.
IJCAR-2008-Otten #agile #logic #performance #proving: leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (JO), pp. 283–291.
IJCAR-2008-PlatzerQ #hybrid #named #proving: KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (AP, JDQ), pp. 171–178.
ILC-2007-Frank #constraints #lisp: Constraint solving in common Lisp (SF), p. 10.
LOPSTR-2007-AbdennadherS #approach #constraints #generative #rule-based: Generation of Rule-Based Constraint Solvers: Combined Approach (SA, IS), pp. 106–120.
LOPSTR-2007-ZhangN #constraints #scalability #unification #using: A Scalable Inclusion Constraint Solver Using Unification (YZ, FN), pp. 121–137.
SAC-2007-DjelloulDF #constraints #finite #first-order #infinity #prolog #towards #unification #using: Toward a first-order extension of Prolog’s unification using CHR: a CHR first-order constraint solver over finite or infinite trees (KD, TBHD, TWF), pp. 58–64.
SAC-2007-KunXY #algorithm #constraints #geometry #parallel: Parallel algorithms on geometric constraint solving (KJ, YG, XL, YZ), pp. 778–779.
CADE-2007-TiwariG #logic #program analysis #proving #using: Logical Interpretation: Static Program Analysis Using Theorem Proving (AT, SG), pp. 147–166.
VMCAI-2007-BouillaguetKWZR #data type #first-order #proving #using #verification: Using First-Order Theorem Provers in the Jahob Data Structure Verification System (CB, VK, TW, KZ, MCR), pp. 74–88.
VMCAI-2007-RybalchenkoS #constraints: Constraint Solving for Interpolation (AR, VSS), pp. 346–362.
FM-2006-UmenoL #automaton #case study #protocol #proving #safety #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 #using #verification: Floating-Point Verification Using Theorem Proving (JH), pp. 211–242.
SFM-2006-Manolios #proving #refinement: Refinement and Theorem Proving (PM), pp. 176–210.
PADL-2006-BecketBMSSW #constraints: Adding Constraint Solving to Mercury (RB, MJGdlB, KM, ZS, PJS, MW), pp. 118–133.
PADL-2006-HawkinsS #constraints #finite #hybrid #satisfiability: A Hybrid BDD and SAT Finite Domain Constraint Solver (PH, PJS), pp. 103–117.
ASE-2006-Jurjens #analysis #automation #java #proving #security #source code #using: Security Analysis of Crypto-based Java Programs using Automated Theorem Provers (JJ), pp. 167–176.
ICSE-2006-ManoliosV #proving #static analysis #termination: Integrating static analysis and general-purpose theorem proving for termination analysis (PM, DV), pp. 873–876.
SAC-2006-Kosmatov #constraints #sequence: A constraint solver for sequences and its applications (NK), pp. 404–408.
SAC-2006-PavonDL #constraints #geometry #problem: An adjustment model in a geometric constraint solving problem (RP, FD, MVL), pp. 968–973.
SAC-2006-ZhangG #composition #constraints #geometry #graph: Spatial geometric constraint solving based on k-connected graph decomposition (GFZ, XSG), pp. 979–983.
CAV-2006-Roe #heuristic #modulo theories #proving #smt: The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover (KR), pp. 467–470.
ISSTA-2006-YorshBS #abstraction #exclamation #proving #testing: Testing, abstraction, theorem proving: better together! (GY, TB, MS), pp. 145–156.
ICALP-2005-DelzannoG #composition #constraints #process #verification: Compositional Verification of Asynchronous Processes via Constraint Solving (GD, MG), pp. 1239–1250.
ICFP-2005-ChenX #programming #proving: Combining programming with theorem proving (CC, HX), pp. 66–77.
SEKE-2005-LiWMW #constraints #generative #testing: A Constraint Solver for Code-based Test Data Generation (JJL, WEW, XM, DMW), pp. 300–305.
ASE-2005-WardKA #framework #named #proving: Prufrock: a framework for constructing polytypic theorem provers (JW, GK, PA), pp. 423–426.
SAC-2005-Goualard #algorithm #constraints #on the: On considering an interval constraint solving algorithm as a free-steering nonlinear Gauss-Seidel procedure (FG), pp. 1434–1438.
DATE-2005-IyerPC #constraints #learning #performance: Efficient Conflict-Based Learning in an RTL Circuit Constraint Solver (MKI, GP, KTC), pp. 666–671.
TACAS-2005-IsobeR #csp #proving #refinement: A Generic Theorem Prover of CSP Refinement (YI, MR), pp. 108–123.
TACAS-2005-LeinoMO #proving #quantifier: A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover (KRML, MM, XO), pp. 334–348.
CADE-2005-CastelliniS #first-order #logic #proving: Proof Planning for First-Order Temporal Logic (CC, AS), pp. 235–249.
CADE-2005-ChaudhuriP #first-order #linear #logic #proving: A Focusing Inverse Method Theorem Prover for First-Order Linear Logic (KC, FP), pp. 69–83.
CADE-2005-MeierM #multi #proving: System Description: Multi A Multi-strategy Proof Planner (AM, EM), pp. 250–254.
CAV-2005-CookKS #named #proving #verification: Cogent: Accurate Theorem Proving for Program Verification (BC, DK, NS), pp. 296–300.
ICLP-2005-BaseliceBG #constraints #integration #set #towards: Towards an Integration of Answer Set and Constraint Solving (SB, PAB, MG), pp. 52–66.
IFM-2004-EllisI #automation #integration #program analysis #proving: An Integration of Program Analysis and Automated Theorem Proving (BJE, AI), pp. 67–86.
IFM-2004-Melham #functional #model checking #proving: Integrating Model Checking and Theorem Proving in a Reflective Functional Language (TFM), pp. 36–39.
SEFM-2004-ZhangXW #constraints #execution #generative #symbolic computation #testing #using: Path-Oriented Test Data Generation Using Symbolic Execution and Constraint Solving Techniques (JZ, CX, XW), pp. 242–250.
ICEIS-v1-2004-Augusto #model checking #verification: Model Checking and Theorem Proving-Based Verification of EIS (JCA), p. XXXIII-XXXIV.
LOPSTR-2004-Colon #constraints #imperative #source code #synthesis: Schema-Guided Synthesis of Imperative Programs by Constraint Solving (MC), pp. 166–181.
DAC-2004-ParthasarathyICW #constraints #performance: An efficient finite-domain constraint solver for circuits (GP, MKI, KTC, LCW), pp. 212–217.
TACAS-2004-LingerS #analysis #constraints #ml #type inference: Binding-Time Analysis for MetaML via Type Inference and Constraint Solving (NL, TS), pp. 266–279.
TACAS-2004-McMillan #proving: An Interpolating Theorem Prover (KLM), pp. 16–30.
CAV-2004-BallCLZ #abstraction #automation #named #proving #refinement: Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement (TB, BC, SKL, LZ), pp. 457–461.
CSL-2004-GanzingerK #equation #proving #reasoning: Integrating Equational Reasoning into Instantiation-Based Theorem Proving (HG, KK), pp. 71–84.
CSL-2004-Lynch #proving: Unsound Theorem Proving (CL), pp. 473–487.
IJCAR-2004-DenneyFS #automation #proving #using: Using Automated Theorem Provers to Certify Auto-generated Aerospace Software (ED, BF, JS), pp. 198–212.
IJCAR-2004-WintersteinBG #diagrams #proving: Dr.Doodle: A Diagrammatic Theorem Prover (DW, AB, CAG), pp. 331–335.
SEFM-2003-DeharbeR #debugging #proving #verification: Light-Weight Theorem Proving for Debugging and Verifying Units of Code (DD, SR), pp. 220–228.
LOPSTR-2003-AbdennadherF #constraints #integration #optimisation #rule-based: Integration and Optimization of Rule-Based Constraint Solvers (SA, TWF), pp. 198–213.
LOPSTR-2003-LehmannL #generative #induction #proving #using: Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce (HL, ML), pp. 1–19.
SAC-2003-MonfroyC #component #constraints: Basic Components for Constraint Solver Cooperations (EM, CC), pp. 367–374.
SAC-2003-Zoeteweij #constraints #coordination #distributed: Coordination-Based Distributed Constraint Solving in DICE (PZ), pp. 360–366.
DAC-2003-ChaiK #constraints #performance #pseudo: A fast pseudo-boolean constraint solver (DC, AK), pp. 830–835.
TACAS-2003-VaziriJ #constraints: Checking Properties of Heap-Manipulating Procedures with a Constraint Solver (MV, DJ), pp. 505–520.
CADE-2003-DixonF #named #prototype #proving: IsaPlanner: A Prototype Proof Planner in Isabelle (LD, JDF), pp. 279–283.
CAV-2003-ColonSS #constraints #generative #invariant #linear #using: Linear Invariant Generation Using Non-linear Constraint Solving (MC, SS, HS), pp. 420–432.
CAV-2003-FlanaganJOS #lazy evaluation #proving #using: Theorem Proving Using Lazy Proof Explication (CF, RJ, XO, JBS), pp. 355–367.
FATES-2003-HahnleW #proving #testing #using: Using a Software Testing Technique to Improve Theorem Proving (RH, AW), pp. 30–41.
LICS-2003-Comon-LundhS #constraints #deduction: Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or (HCL, VS), p. 271–?.
LICS-2003-GanzingerK #proving: New Directions in Instantiation-Based Theorem Proving (HG, KK), pp. 55–64.
LOPSTR-2002-AbdennadherR #constraints #logic programming #synthesis #using: Constraint Solver Synthesis Using Tabled Resolution for Constraint Logic Programming (SA, CR), pp. 32–47.
DATE-2002-FerrandiRS #constraints #functional #using #verification: Functional Verification for SystemC Descriptions Using Constraint Solving (FF, MR, DS), pp. 744–751.
TACAS-2002-BouquetLP #constraints #named: CLPS-B — A Constraint Solver for B (FB, BL, FP), pp. 188–204.
CADE-2002-Brown #higher-order #proving #set: Solving for Set Variables in Higher-Order Theorem Proving (CEB), pp. 408–422.
CADE-2002-MouraRS #bound #infinity #lazy evaluation #model checking #proving: Lazy Theorem Proving for Bounded Model Checking over Infinite Domains (LMdM, HR, MS), pp. 438–455.
TestCom-2002-CastanetR #analysis #proving #reachability #testing: Generate Certified Test Cases by Combining Theorem Proving and Reachability Analysis (RC, DR), pp. 249–266.
ICALP-2001-KorovinV #constraints: Knuth-Bendix Constraint Solving Is NP-Complete (KK, AV), pp. 979–992.
IFL-2001-MolEP #functional #proving: Theorem Proving for Functional Programmers (MdM, MCJDvE, MJP), pp. 55–71.
PPDP-2001-AbdennadherR #confluence #constraints #rule-based #using: Using Confluence to Generate Rule-Based Constraint Solvers (SA, CR), pp. 127–135.
ASE-2001-CookIM #higher-order #proving #synthesis: Higher Order Function Synthesis Through Proof Planning (AC, AI, GM), pp. 307–310.
ESEC-FSE-2001-EdvardssonK #analysis #constraints #generative #testing: Analysis of the constraint solver in UNA based test data generation (JE, MK), pp. 237–245.
CAV-2001-Bertot #formal method #proving #verification: Formalizing a JVML Verifier for Initialization in a Theorem Prover (YB), pp. 14–24.
ICLP-2001-BandaJMNSH #constraints: Building Constraint Solvers with HAL (MJGdlB, DJ, KM, NN, PJS, CH), pp. 90–104.
IJCAR-2001-Beeson #higher-order #proving: A Second-Order Theorem Prover Applied to Circumscription (MB), pp. 318–324.
IJCAR-2001-Happe #proving: The MODPROF Theorem Prover (JH), pp. 459–463.
IJCAR-2001-HodasT #agile #first-order #implementation #linear #logic #named #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: DCTP — A Disconnection Calculus Theorem Prover — System Abstract (RL, GS), pp. 381–385.
IJCAR-2001-NieuwenhuisHRV #evaluation #on the #proving: On the Evaluation of Indexing Techniques for Theorem Proving (RN, TH, AR, AV), pp. 257–271.
IJCAR-2001-Pastre #deduction #knowledge-based #proving: MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction (DP), pp. 685–689.
IJCAR-2001-SchmittLKN #interactive #proving: JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants (SS, LL, CK, AN), pp. 421–426.
SAT-2001-McllraithA #proving: Theorem Proving with Structured Theories (Preliminary Report)* (SM, EA), pp. 311–328.
UML-2000-Padawitz #constraints #diagrams #how #proving #state machine #uml: Swinging UML: How to Make Class Diagrams and State Machines Amenable to Constraint Solving and Proving (PP), pp. 162–177.
PADL-2000-Hickey #constraints #named: CLIP: A CLP(Intervals) Dialect for Metalevel Constraint Solving (TJH), pp. 200–214.
POPL-2000-Hickey #constraints: Analytic Constraint Solving and Interval Arithmetic (TJH), pp. 338–351.
SAS-2000-Podelski #constraints #model checking: Model Checking as Constraint Solving (AP), pp. 22–37.
TACAS-2000-BharadwajS #automation #constraints #invariant #named: Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking (RB, SS), pp. 378–394.
CADE-2000-AndrewsB #education #higher-order #logic #named #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 #type system: System Description: TPS: A Theorem Proving System for Type Theory (PBA, MB, CEB), pp. 164–169.
CADE-2000-Harrison #proving #using #verification: High-Level Verification Using Theorem Proving and Formalized Mathematics (JH), pp. 1–6.
CADE-2000-NeculaL #generative #proving: Proof Generation in the Touchstone Theorem Prover (GCN, PL), pp. 25–44.
CADE-2000-Seger #float #model checking #proving: Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice (CJHS), p. 235.
CADE-2000-Sinz #algebra #automation #proving: System Description: ARA — An Automatic Theorem Prover for Relation Algebras (CS), pp. 177–182.
CL-2000-HahnleHS #constraints #finite #generative #proving: Moder Generation Theorem Proving with Finite Interval Constraints (RH, RH, YS), pp. 285–299.
CL-2000-MelisM #multi #proving: Proof Planning with Multiple Strategies (EM, AM), pp. 644–659.
ISSTA-2000-JacksonV #constraints #debugging: Finding bugs with a constraint solver (DJ, MV), pp. 14–25.
WICSA-1999-HirschIM #constraints #graph grammar #modelling: Modeling Software Architecutes and Styles with Graph Grammars and Constraint Solving (DH, PI, UM), pp. 127–144.
FM-v2-1999-Nadjm-TehraniA #design #modelling #proving: Combining Theorem Proving and Continuous Models in Synchronous Design (SNT, OÅ), pp. 1384–1399.
FLOPS-1999-FernandezH #constraints #framework: An Interval Lattice-Based Constraint Solving Framework for Lattices (AJF, PMH), pp. 194–208.
ASE-1999-StarkI #automation #imperative #proving #synthesis #towards: Towards Automatic Imperative Program Synthesis Through Proof Planning (JS, AI), pp. 44–51.
FASE-1999-LuthTKK #development #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: On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction (VR, ES), pp. 178–192.
TACAS-1999-SpeltE #analysis #database #object-oriented: A Theorem Prover-Based Analysis Tool for Object-Oriented Databases (DS, SE), pp. 375–389.
CADE-1999-Artemov #on the #proving #verification: On Explicit Reflection in Theorem Proving and Formal Verification (SNA), pp. 267–281.
CADE-1999-FrankeK #automation #communication #distributed #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: Fault-Tolerant Distributed Theorem Proving (JH), pp. 227–231.
CADE-1999-HutterB #contest #design #induction #proving: The Design of the CADE-16 Inductive Theorem Prover Contest (DH, AB), pp. 374–377.
CADE-1999-JanicicBG #flexibility #framework #integration #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: Invited Talk: Embedding Programming Languages in Theorem Provers (TN), p. 398.
CADE-1999-Voronkov #named #proving: KK: a theorem prover for K (AV), pp. 383–387.
CAV-1999-ManoliosNS #bisimulation #model checking #proving: Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation (PM, KSN, RS), pp. 369–379.
CSL-1999-Howe #interactive #proving #type system #using: Interactive Theorem Proving Using Type Theory (DJH), p. 578.
ICLP-1999-DemoenBHMS #constraints: Herbrand Constraint Solving in HAL (BD, MJGdlB, WH, KM, PJS), pp. 260–274.
CSMR-1998-JakobiW #automation #database #evaluation #framework #maintenance #named #proving: DBFW: A Simple DataBase FrameWork for the Evaluation and Maintenance of Automated Theorem Prover Data (PJ, AW), pp. 185–188.
ICALP-1998-Lugiez #automaton #induction #proving: A Good Class of Tree Automata and Application to Inductive Theorem Proving (DL), pp. 409–420.
LOPSTR-1998-GabricGS #analysis #constraints #strict: Strictness Analysis as Finite-Domain Constraint Solving (TG, KG, HS), pp. 255–270.
LOPSTR-1998-Richardson #named #proving: Abstract: Proof Planning with Program Schemas (JR), pp. 313–315.
ASE-1998-Ledru #identification #proving: Identifying Pre-Conditions with the Z/EVES Theorem Prover (YL), p. 32–?.
SAC-1998-ArbabM #constraints #coordination #using: Using coordination for cooperative constraint solving (FA, EM), pp. 139–148.
DAC-1998-AagaardJS #evaluation #industrial #proving: Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment (MA, RBJ, CJHS), pp. 538–541.
WRLA-1998-BorovanskyC #constraints #process #using: Cooperation of constraint solvers: using the new process control facilities of ELAN (PB, CC), pp. 1–20.
CADE-1998-BenzmullerK98a #higher-order #proving: System Description: LEO — A Higher-Order Theorem Prover (CB, MK), pp. 139–144.
CADE-1998-FleuriotP #analysis #geometry #proving #standard: 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: System Description: card TAP: The First Theorem Prover on a Smart Card (RG, JP, AS, HV), pp. 47–50.
CADE-1998-RichardsonSG #higher-order #logic #proving: System Description: Proof Planning in Higher-Order Logic with Lambda-Clam (JR, AS, IG), pp. 129–133.
CADE-1998-SchurmannP #automation #logic #proving: Automated Theorem Proving in a Simple Meta-Logic for LF (CS, FP), pp. 286–300.
CAV-1998-Camilleri #design #multi #proving: A Role for Theorem Proving in Multi-Processor Design (AJC), pp. 45–48.
CAV-1998-HardinWG #concept #design #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-NarendranRV #constraints: RPO Constraint Solving Is in NP (PN, MR, RMV), pp. 385–398.
ISSTA-1998-GotliebBR #automation #constraints #generative #testing #using: Automatic Test Data Generation Using Constraint Solving Techniques (AG, BB, MR), pp. 53–62.
FME-1997-AgerholmF #automation #proving #towards: Towards an Integrated CASE and Theorem Proving Tool for VDM-SL (SA, JF), pp. 278–297.
RTA-1997-KuhlerW #data type #equation #induction #proving #specification: Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving (UK, CPW), pp. 38–52.
TLCA-1997-Ruess #calculus #proving: Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving (HR), pp. 319–335.
PLILP-1997-CarlssonOC #constraints #finite: An Open-Ended Finite Domain Constraint Solver (MC, GO, BC), pp. 191–206.
TACAS-1997-SandnerM #proving #refinement: Theorem Prover Support for the Refinement of Stream Processing Functions (RS, OM), pp. 351–365.
TAPSOFT-1997-KolyangLMW #development #interface #proving: TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving (K0, CL, TM0, BW), pp. 855–858.
CADE-1997-Bonacina #proving: The Clause-Diffusion Theorem Prover Peers-mcd (MPB), pp. 53–56.
CADE-1997-DahnGHW #automation #integration #interactive #proving: Integration of Automated and Interactive Theorem Proving in ILP (BID, JG, TH, AW), pp. 57–60.
CADE-1997-FeltyH #hybrid #interactive #proving #using: Hybrid Interactive Theorem Proving Using Nuprl and HOL (APF, DJH), pp. 351–365.
CADE-1997-HasegawaIOK #bottom-up #proving #set #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 #top-down: Lemma Matching for a PTTP-based Top-down Theorem Prover (KI), pp. 146–160.
CADE-1997-LoweD #named #proving: XBarnacle: Making Theorem Provers More Accessible (HL, DD), pp. 404–407.
CADE-1997-Slaney #logic #named #proving: Minlog: A Minimal Logic Theorem Prover (JKS), pp. 268–271.
CAV-1997-ChanABN #constraints #model checking: Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints (WC, RJA, PB, DN), pp. 316–327.
ICALP-1996-Ganzinger #proving: Saturation-Based Theorem Proving (HG), pp. 1–3.
FME-1996-HavelundS #model checking #protocol #proving #verification: Experiments in Theorem Proving and Model Checking for Protocol Verification (KH, NS), pp. 662–681.
RTA-1996-BoudetCM #proving #unification: AC-Complete Unification and its Application to Theorem Proving (AB, EC, CM), pp. 18–32.
RTA-1996-HillenbrandBF #on the #performance #proving: On Gaining Efficiency in Completion-Based Theorem Proving (TH, AB, RF), pp. 432–435.
RTA-1996-Stuber #integer #proving: Superposition Theorem Proving for Albelian Groups Represented as Integer Modules (JS), pp. 33–47.
ALP-1996-Benhamou #constraints: Heterogeneous Constraint Solving (FB), pp. 62–76.
PLILP-1996-StuckeyT #constraints #logic programming #modelling #probability #using: Models for Using Stochastic Constraint Solvers in Constraint Logic Programming (PJS, VT), pp. 423–437.
SAS-1996-Snelting #constraints #metric #slicing #validation: Combining Slicing and Constraint Solving for Validation of Measurement Software (GS), pp. 332–348.
CADE-1996-BeckertHOS #proving: The Tableau-based Theorem Prover 3TAP Version 4.0 (BB, RH, PO, MS), pp. 303–307.
CADE-1996-DenzingerS #learning #proving: Learning Domain Knowledge to Improve Theorem Proving (JD, SS), pp. 62–76.
CADE-1996-Ganzinger #proving: Saturation-Based Theorem Proving: Past Successes and Future Potential (HG), p. 1.
CADE-1996-GanzingerW #monad #proving: Theorem Proving in Cancellative Abelian Monoids (HG, UW), pp. 388–402.
CADE-1996-KolbeW #proving #reuse #termination: Termination of Theorem Proving by Reuse (TK, CW), pp. 106–120.
CADE-1996-Luz-Filho #logic #proving #specification: Grammar Specification in Categorial Logics and Theorem Proving (SFLF), pp. 703–717.
CADE-1996-Martin #proving: Theorem Proving with Group Presentations: Examples and Questions (UM), pp. 358–372.
CADE-1996-MelisW #proving: Internal Analogy in Theorem Proving (EM, JW), pp. 92–105.
CADE-1996-SchaubBN #named #prolog #proving #reasoning: XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description (TS, SB, PN), pp. 293–297.
CADE-1996-Schumann #named #parallel #proving: SiCoTHEO: Simple Competitive Parallel Theorem Provers (JS), pp. 240–244.
CADE-1996-Tammet #logic #proving: A Resolution Theorem Prover for Intuitonistic Logic (TT), pp. 2–16.
CADE-1996-Wang #geometry #named #proving: GEOTHER: A Geometry Theorem Prover (DW), pp. 166–170.
CAV-1996-ClarkeGZ #algorithm #proving #using #verification: Verifying the SRT Division Algorithm Using Theorem Proving Techniques (EMC, SMG, XZ), pp. 111–122.
CAV-1996-GrafS #invariant #proving #using #verification: Verifying Invariants Using theorem Proving (SG, HS), pp. 196–207.
RTA-1995-BaaderS #algebra #constraints #perspective: Combination of Constraint Solving Techniques: An Algebraic POint of View (FB, KUS), pp. 352–366.
RTA-1995-Stickel #proving #term rewriting: Term Rewriting in Contemporary Resolution Theorem Proving (MES), p. 101.
PEPM-1995-RamakrishnanRS #analysis #constraints #framework #logic programming #source code: A Symbolic Constraint Solving Framework for Analysis of Logic Programs (CRR, IVR, RCS), pp. 12–23.
CAV-1995-DingelF #abstraction #infinity #model checking #proving #reasoning #using: Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving (JD, TF), pp. 54–69.
ICLP-1995-ChiuL #constraints #linear #using: Interval Linear Constraint Solving Using the Preconditioned Interval Gauss-Seidel Method (CKC, JHML), pp. 17–31.
ICLP-1995-FormicaMT #database #object-oriented #proving #satisfiability: A Theorem Prover for Checking Satisfiability of Object-Oriented Database Schemas (AF, MM, RT), p. 819.
ICLP-1995-Hasegawa #generative #proving: Model Generation Theorem Provers and Their Applications (RH), p. 7.
LICS-1995-ComonNR #constraints #order: Orderings, AC-Theories and Symbolic Constraint Solving (HC, RN, AR), pp. 375–385.
PLILP-1994-CodognetD #constraints #performance: clp(B): Combining Simplicity and Efficiency in Boolean Constraint Solving (PC, DD), pp. 244–260.
CADE-1994-BeckertP #agile #named #proving: leanTAP: Lean Tableau-Based Theorem Proving (BB, JP), pp. 793–797.
CADE-1994-BonacinaM #distributed #proving: Distributed Theorem Proving by Peers (MPB, WM), pp. 841–845.
CADE-1994-ChuP #first-order #proving #semantics #using: Semantically Guided First-Order Theorem Proving using Hyper-Linking (HC, DAP), pp. 192–206.
CADE-1994-ClarkeZ #problem #proving #symbolic computation: Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan (EMC, XZ), pp. 758–763.
CADE-1994-FeltyH #proving: Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables (APF, DJH), pp. 605–619.
CADE-1994-Plaisted #performance #proving: The Search Efficiency of Theorem Proving Strategies (DAP), pp. 57–71.
CADE-1994-Schumann #bottom-up #named #preprocessor #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: The Applicability of Logic Program Analysis and Transformation to Theorem Proving (DAdW, JPG), pp. 207–221.
ICLP-1994-KirchnerR #algebra #constraints: Constraint Solving by Narrowing in Combined Algebraic Domains (HK, CR), pp. 617–631.
ILPS-1994-ChiuL #constraints #logic programming #towards: Towards Practical Interval Constraint Solving in Logic Programming (CKC, JHML), pp. 109–123.
RTA-1993-AvenhausD #equation #proving: Distributing Equational Theorem Proving (JA, JD), pp. 62–76.
RTA-1993-Bachmair #proving: Rewrite Techniques in Theorem Proving (LB), p. 1.
LOPSTR-1993-MaddenHGB #automation #generative #performance #proving #source code #using: A General Technique for Automatically Generating Efficient Programs Through the Use of Proof Planning (PM, JH, IG, AB), pp. 64–66.
PLILP-1993-CorsiniMRC #abstract interpretation #bottom-up #constraints #finite #performance #prolog: Efficient Bottom-up Abstract Interpretation of Prolog by Means of Constraint Solving over Symbolic Finite Domains (MMC, KM, AR, BLC), pp. 75–91.
CAV-1993-Hungar #model checking #parallel #process #proving #verification: Combining Model Checking and Theorem Proving to Verify Parallel Processes (HH), pp. 154–165.
ILPS-1993-CodognetD #constraints #using: Boolean Constraint Solving Using clp(FD) (PC, DD), pp. 525–539.
KR-1992-Lamarre #proving: A Promenade from Monotonicity to Non-Monotonicity Following a Theorem Prover (PL), pp. 572–580.
ALP-1992-BachmairGW #first-order #proving: Theorem Proving for Hierarchic First-Order Theories (LB, HG, UW), pp. 420–434.
LOPSTR-1992-KraanBB #logic programming #proving #synthesis: Logic Program Synthesis via Proof Planning (IK, DAB, AB), pp. 1–14.
ESOP-1992-Gnaedig #proving #specification: ELIOS-OBJ Theorem Proving in a Specification Language (IG), pp. 182–199.
CADE-1992-AstrachanS #proving: Caching and Lemmaizing in Model Elimination Theorem Provers (OLA, MES), pp. 224–238.
CADE-1992-Baker-PlummerR #proving: The GAZER Theorem Prover (DBP, AR), pp. 726–730.
CADE-1992-BeckertGHK #logic #multi #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: Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic (WZC), pp. 552–566.
CADE-1992-Chou #geometry #proving: A Geometry Theorem Prover for Macintoshes (SCC), pp. 686–690.
CADE-1992-ClarkeZ #named #proving: Analytica — A Theorem Prover in Mathematica (EMC, XZ), pp. 761–765.
CADE-1992-Dafa #automation #deduction #proving: A Natural Deduction Automated Theorem Proving System (LD), pp. 668–672.
CADE-1992-HasegawaKF #generative #lazy evaluation #named #parallel #proving: MGTP: A Parallel Theorem Prover Based on Lazy Model Generation (RH, MK, HF), pp. 776–780.
CADE-1992-InoueKH #generative #proving: Embedding Negation as Failure into a Model Generation Theorem Prover (KI, MK, RH), pp. 400–415.
CADE-1992-LuskMS #named #parallel #proving: ROO: A Parallel Theorem Prover (ELL, WM, JKS), pp. 731–734.
CADE-1992-NieuwenhuisR #proving: Theorem Proving with Ordering Constrained Clauses (RN, AR), pp. 477–491.
CADE-1992-RandellCC #automation #challenge #proving: Computing Transivity Tables: A Challenge For Automated Theorem Provers (DAR, AGC, ZC), pp. 786–790.
CADE-1992-Schumann #logic #named #proving: KPROP — An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (JS), pp. 740–742.
CADE-1992-Voronkov #logic #proving #standard: Theorem Proving in Non-Standard Logics Based on the Inverse Method (AV), pp. 648–662.
CADE-1992-WalshNB #proving #using: The Use of Proof Plans to Sum Series (TW, AN, AB), pp. 325–339.
CAV-1992-WrightL #algorithm #concurrent #proving #reasoning #using: Using a Theorem Prover for Reasoning about Concurrent Algorithms (JvW, TL), pp. 56–68.
JICSLP-1992-KirchnerR #algebra #algorithm #constraints #finite #unification: A Constraint Solver in Finite Algebras and Its Combination with Unification Algorithms (HK, CR), pp. 225–239.
RTA-1991-BonacinaH #on the #proving: On Fairness of Completion-Based Theorem Proving Strategies (MPB, JH), pp. 348–360.
RTA-1991-Deruyver #equation #first-order #logic #named #proving: EMMY: A Refutational Theorem Prover for First-Order Logic with Equation (AD), pp. 439–441.
RTA-1991-Fraus #proving: A Narrowing-Based Theorem Prover (UF), pp. 435–436.
KR-1991-HalpernV #model checking #proving: Model Checking vs. Theorem Proving: A Manifesto (JYH, MYV), pp. 325–334.
OOPSLA-1991-Wilk #constraints #named #object-oriented: Equate: An Object-Oriented Constraint Solver (MRW), pp. 286–298.
PLILP-1991-FrausH #proving: A Narrowing-Based Theorem Prover (UF, HH), pp. 421–422.
ICLP-1991-FujitaH #algorithm #generative #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 #unification: Higher-Order Unification as a Theorem Proving Procedure (MH), pp. 270–284.
PLILP-1990-Jaakola #algorithm #constraints: Modifying the Simplex Algorithm to a Constraint Solver (JJ), pp. 89–105.
ICSE-1990-LafontaineLS #case study #development #empirical #formal method #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: The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 641–642.
CADE-1990-BoyerM #logic #proving: A Theorem Prover for a Computational Logic (RSB, JSM), pp. 1–15.
CADE-1990-ButlerFJO #parallel #proving: A High-Performance Parallel Theorem Prover (RB, ITF, AJ, RAO), pp. 649–650.
CADE-1990-ChouG #algorithm #composition #geometry #proving: Ritt-Wu’s Decomposition Algorithm and Geometry Theorem Proving (SCC, XSG), pp. 207–220.
CADE-1990-CostaHLS #automation #implementation #logic #proving: Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation (NCAdC, LJH, JJL, VSS), pp. 72–86.
CADE-1990-Gramlich #induction #named #proving: UNICOM: A Refined Completion Based Inductive Theorem Prover (BG), pp. 655–656.
CADE-1990-HeiselRS #proving #verification: Tactical Theorem Proving in Program Verification (MH, WR, WS), pp. 117–131.
CADE-1990-HsiangJ #proving #tutorial: Tutorial on Rewrite-Based Theorem Proving (JH, JPJ), p. 684.
CADE-1990-KaflZ #proving #verification: The Theorem Prover of the Program Verifier Tatzelwurm (TK, NZ), pp. 657–658.
CADE-1990-LuskM #automation #proving #tutorial: Tutorial on High-Performance Automated Theorem Proving (ELL, WM), p. 681.
CADE-1990-MurrayR #named #proving: DISSOLVER: A Dissolution-based Theorem Prover (NVM, ER), pp. 665–666.
CADE-1990-SchumannL #named #parallel #proving: PARTHEO: A High-Performance Parallel Theorem Prover (JS, RL), pp. 40–56.
CADE-1990-SchumannLK #implementation #parallel #performance #proving #tutorial: Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation (JS, RL, FJK), p. 683.
CADE-1990-Schwind #decidability #logic #proving #set: A Tableau-Based Theorem Prover for a Decidable Subset of Default Logic (CS), pp. 528–542.
CADE-1990-Stickel #prolog #proving: A Prolog Technology Theorem Prover (MES), pp. 673–674.
CADE-1990-Sutcliffe #proving: A General Clause Theorem Prover (GS), pp. 675–676.
CADE-1990-Tuominen #framework #logic #proving: Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic (HT), pp. 514–527.
RTA-1989-AvenhausDM #named #performance #proving: THEOPOGLES — An efficient Theorem Prover based on Rewrite-Techniques (JA, JD, JM), pp. 538–541.
RTA-1989-BonacinaS #equation #named #proving: KBlab: An Equational Theorem Prover for the Macintosh (MPB, GS), pp. 548–550.
LICS-1989-BoseCLM #horn clause #named #parallel #proving: PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (SB, EMC, DEL, SM), pp. 80–89.
SIGMOD-1988-MazumdarSS #proving #security #using: Resolving the Tension between Integrity and Security Using a Theorem Prover (SM, DWS, TS), pp. 233–242.
VDME-1988-JonesM #design #empirical #named #proving #user interface: MUFFIN: A User Interface Design Experiment for a Theorem Proving Assistant (CBJ, RCM), pp. 337–375.
CADE-1988-AllenBCM #horn clause #named #parallel #proving: PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (PEA, SB, EMC, SM), pp. 764–765.
CADE-1988-AndrewsINP #proving: The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 760–761.
CADE-1988-BrownP #logic #named #proving: SYMEVAL: A Theorem Prover Based on the Experimental Logic (FMB, SSP), pp. 756–757.
CADE-1988-CyrlukHK #algebra #geometry #named #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: Specifying Theorem Provers in a Higher-Order Logic Programming Language (APF, DM), pp. 61–80.
CADE-1988-Hines #knowledge-based #proving: Hyper-Chaining and Knowledge-Based Theorem Proving (LMH), pp. 469–486.
CADE-1988-Kaufmann #interactive #proving: An Interactive Enhancement to the Boyer-Moore Theorem Prover (MK), pp. 735–736.
CADE-1988-MantheyB #named #prolog #proving: SATCHMO: A Theorem Prover Implemented in Prolog (RM, FB), pp. 415–434.
CADE-1988-McRobbieMT #automation #knowledge-based #logic #performance #proving #standard #towards: Towards Efficient “Knowledge-Based” Automated Theorem Proving for Non-Standard Logics (MAM, RKM, PBT), pp. 197–217.
CADE-1988-Paulson #named #proving: Isabelle: The Next Seven Hundred Theorem Provers (LCP), pp. 772–773.
CADE-1988-Plaisted #proving: A Goal Directed Theorem Prover (DAP), p. 737.
CADE-1988-Stevens #challenge #problem #proving: Challenge Problems from Nonassociative Rings for Theorem Provers (RLS), pp. 730–734.
CADE-1988-Stickel88a #prolog #proving: A Prolog Technology Theorem Prover (MES), pp. 752–753.
CADE-1988-ZhangK #first-order #proving #using: First-Order Theorem Proving Using Conditional Rewrite Rules (HZ, DK), pp. 1–20.
LICS-1987-BachmairD #first-order #proving: Inference Rules for Rewrite-Based First-Order Theorem Proving (LB, ND), pp. 331–337.
LICS-1987-GallierRS #equation #proving #using: Theorem Proving Using Rigid E-Unification Equational Matings (JHG, SR, WS), pp. 338–346.
CADE-1986-AbadiM #proving: Modal Theorem Proving (MA, ZM), pp. 172–189.
CADE-1986-AndrewsPIK #proving: The TPS Theorem Proving System (PBA, FP, SI, CPK), pp. 663–664.
CADE-1986-BeierleOV #automation #proving: Automatic Theorem Proving in the ISDV System (CB, WGO, AV), pp. 670–671.
CADE-1986-BiundoHHW #induction #proving: The Karlsruhe Induction Theorem Proving System (SB, BH, DH, CW), pp. 672–674.
CADE-1986-ButlerLMO #automation #proving: Paths to High-Performance Automated Theorem Proving (RB, ELL, WM, RAO), pp. 588–597.
CADE-1986-Chou #geometry #named #proving: GEO-Prover — A Geometry Theorem Prover Developed at UT (SCC), pp. 679–680.
CADE-1986-GreenbaumP #proving: The Illinois Prover: A General Purpose Resolution Theorem Prover (SG, DAP), pp. 685–687.
CADE-1986-HsiangR #proving: A New Method for Establishing Refutational Completeness in Theorem Proving (JH, MR), pp. 141–152.
CADE-1986-Huet86a #proving: Theorem Proving Systems of the Formel Project (GPH), pp. 687–688.
CADE-1986-KutzlerS #algorithm #geometry #proving: A Geometry Theorem Prover Based on Buchberger’s Algorithm (BK, SS), pp. 693–694.
CADE-1986-LoganantharajM #graph #parallel #proving: Parallel Theorem Proving with Connection Graphs (RL, RAM), pp. 337–352.
CADE-1986-Stickel #compilation #implementation #prolog #proving: A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler (MES), pp. 573–587.
CADE-1986-ThistlewaiteMM #automation #proving: The KRIPKE Automated Theorem Proving System (PBT, MAM, RKM), pp. 705–706.
LICS-1986-ChouK #geometry #on the #proving: On Mechanical Theorem Proving in Minkowskian Plane Geometry (SCC, HPK), pp. 187–192.
RTA-1985-Hsiang #proving #term rewriting: Two Results in Term Rewriting Theorem Proving (JH), pp. 301–324.
CADE-1984-OhlbachW #automation #logic #problem #proving: Solving a Problem in Relevance Logic with an Automated Theorem Prover (HJO, GW), pp. 496–508.
CADE-1984-Plaisted #analysis #dependence #graph #proving #using: Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving (DAP), pp. 356–374.
CADE-1984-Stickel #case study #commutative #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: The Next Generation of Interactive Theorem Provers (PS), pp. 303–315.
SLP-1984-Stickel84 #prolog #proving: A Prolog Technology Theorem Prover (MES), pp. 211–217.
ICALP-1983-HsiangD #proving: Rewrite Methods for Clausal and Non-Clausal Theorem Proving (JH, ND), pp. 331–346.
ICALP-1980-Turchin #optimisation #proving #using: The Use of Metasystem Transition in Theorem Proving and Program Optimization (VFT), pp. 645–657.
CADE-1980-EricksonM #proving #scalability: The AFFIRM Theorem Prover: Proof Forests and Management of Large Proofs (RWE, DRM), pp. 220–231.
CADE-1980-Gloess #correctness #empirical #parsing #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 #λ-calculus: An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus (RN), pp. 182–194.
CADE-1980-Plaisted #abstraction #proving: Abstraction Mappings in Mechanical Theorem Proving (DAP), pp. 264–280.
ICALP-1976-Galil #integer #on the #programming #proving: On Enumeration Procedures for Theorem Proving and for Integer Programming (ZG), pp. 355–381.
STOC-1970-KingF #integer #proving: An Interpretation Oriented Theorem Prover over Integers (JCK, RWF), pp. 169–179.
STOC-1970-Reiter #proving: The Predicate Elimination Strategy in Theorem Proving (RR), pp. 180–183.