Stem prover$ (all stems)

166 papers:

ICALP-v1-2015-CoudronV #approximate #interactive #proving

Interactive Proofs with Approximately Commuting Provers (MC, TV), pp. 355–366.

CADE-2015-BaumgartnerBW #named #proving #theorem proving

Beagle — A Hierarchic Superposition Theorem Prover (PB, JB, UW), pp. 367–377.

CADE-2015-FultonMQVP #axiom #hybrid #proving #theorem proving

KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (NF, SM, JDQ, MV, AP), pp. 527–538.

CADE-2015-MouraKADR #agile #proving #theorem proving

The Lean Theorem Prover (System Description) (LMdM, SK, JA, FvD, JvR), pp. 378–388.

IFM-2014-ChaudhariD #automation #proving #theorem proving

Automated Theorem Prover Assisted Program Calculations (DLC, OPD), pp. 205–220.

CAV-2014-Voronkov #architecture #first-order #named #proving #theorem proving

AVATAR: The Architecture for First-Order Theorem Provers (AV), pp. 696–710.

IJCAR-2014-GoreTW #logic #proving #theorem proving #using

A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description (RG, JT, JW), pp. 262–268.

IJCAR-2014-Otten #first-order #logic #named #proving

MleanCoP: A Connection Prover for First-Order Modal Logic (JO), pp. 269–276.

ESOP-2013-FilliatreP #named #proving #source code #why

Why3 — Where Programs Meet Provers (JCF, AP), pp. 125–128.

POPL-2013-ParkSP #proving #theorem proving

A theorem prover for Boolean BI (JP, JS, SP), pp. 219–232.

CADE-2013-HawblitzelKLR #automation #proving #source code #theorem proving #towards #using

Towards Modularly Comparing Programs Using Automated Theorem Provers (CH, MK, SKL, HR), pp. 282–299.

CAV-2013-MeierSCB #analysis #protocol #proving #security

The TAMARIN Prover for the Symbolic Analysis of Security Protocols (SM, BS, CC, DAB), pp. 696–701.

TACAS-2012-SonnexDE #automation #data type #named #proving #recursion

Zeno: An Automated Prover for Properties of Recursive Data Structures (WS, SD, SE), pp. 407–421.

ICFP-2012-StewartBA #proving #theorem proving

Verified heap theorem prover by paramodulation (GS, LB, AWA), pp. 3–14.

POPL-2012-Moore #proving #theorem proving

Meta-level features in an industrial-strength theorem prover (JSM), pp. 425–426.

IJCAR-2012-Brown #automation #higher-order #named #proving

Satallax: An Automatic Higher-Order Prover (CEB), pp. 111–117.

IJCAR-2012-JacquelBDD #automation #deduction #modulo theories #proving #theorem proving #using #verification

Tableaux Modulo Theories Using Superdeduction — An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover (MJ, KB, DD, CD), pp. 332–338.

IJCAR-2012-SudaW

A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance (MS, CW), pp. 537–543.

PLDI-2011-PerezR #calculus #logic #proving #theorem proving

Separation logic + superposition calculus = heap theorem prover (JANP, AR), pp. 556–566.

CADE-2011-AspertiRCT #interactive #proving #theorem proving

The Matita Interactive Theorem Prover (AA, WR, CSC, ET), pp. 64–69.

CADE-2011-BohmeM #automation #challenge #data type #proving

Heaps and Data Structures: A Challenge for Automated Provers (SB, MM), pp. 177–191.

ICALP-v1-2010-Ito #approximate #proving

Polynomial-Space Approximation of No-Signaling Provers (TI), pp. 140–151.

CSL-2010-Burel #deduction #proving

Embedding Deduction Modulo into a Prover (GB), pp. 155–169.

IJCAR-2010-AyadM #float #multi #source code #verification

Multi-Prover Verification of Floating-Point Programs (AA, CM), pp. 127–141.

IJCAR-2010-KorovinS #named #proving #similarity #theorem proving

iProver-Eq: An Instantiation-Based Theorem Prover with Equality (KK, CS), pp. 196–202.

IJCAR-2010-MayerC #hybrid #logic #proving

Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic (MCM, SC), pp. 255–262.

FASE-2009-KovacsV #array #invariant #proving #source code #theorem proving #using

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover (LK, AV), pp. 470–485.

SAC-2009-JamesC #ml #multi #static analysis

Extended static checking in JML4: benefits of multiple-prover support (PRJ, PC), pp. 609–614.

CADE-2009-BensaidCP #integer #named #proving #theorem proving

Dei: A Theorem Prover for Terms with Integer Exponents (HB, RC, NP), pp. 146–150.

CADE-2009-Stickel #proving #theorem proving

Building Theorem Provers (MES), pp. 306–321.

TestCom-FATES-2009-SubramaniamXGP #approach #proving #testing #theorem proving #using

An Approach for Test Selection for EFSMs Using a Theorem Prover (MS, LX, BG, ZP), pp. 146–162.

TACAS-2008-McMillan #generative #invariant #proving #quantifier #using

Quantified Invariant Generation Using an Interpolating Saturation Prover (KLM), pp. 413–427.

SEFM-2008-GuoS #finite #impact analysis #proving #state machine #theorem proving #using

Formal Change Impact Analyses of Extended Finite State Machines Using a Theorem Prover (BG, MS), pp. 335–344.

SAC-2008-AbedMS #analysis #graph #multi #proving #reachability #theorem proving #using

Reachability analysis using multiway decision graphs in the HOL theorem prover (SA, OAM, GAS), pp. 333–338.

CAV-2008-MeikleF #approach #proving #verification

Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B (LIM, JDF), pp. 309–313.

ICLP-2008-NearBF #declarative #first-order #logic #named #proving #theorem proving

αleanTAP: A Declarative Theorem Prover for First-Order Classical Logic (JPN, WEB, DPF), pp. 238–252.

IJCAR-2008-BenzmullerPTF #automation #higher-order #logic #named #proving #theorem proving

LEO-II — A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) (CB, LCP, FT, AF), pp. 162–170.

IJCAR-2008-Gacek #interactive #proving #theorem proving

The Abella Interactive Theorem Prover (System Description) (AG), pp. 154–161.

IJCAR-2008-Korovin #first-order #logic #named #proving #theorem proving

iProver — An Instantiation-Based Theorem Prover for First-Order Logic (System Description) (KK), pp. 292–298.

IJCAR-2008-PlatzerQ #hybrid #named #proving #theorem proving

KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) (AP, JDQ), pp. 171–178.

VMCAI-2007-BouillaguetKWZR #data type #first-order #proving #theorem proving #using #verification

Using First-Order Theorem Provers in the Jahob Data Structure Verification System (CB, VK, TW, KZ, MCR), pp. 74–88.

ASE-2006-Jurjens #analysis #automation #java #proving #security #source code #theorem proving #using

Security Analysis of Crypto-based Java Programs using Automated Theorem Provers (JJ), pp. 167–176.

STOC-2006-NguyenV #performance #proving

Zero knowledge with efficient provers (MHN, SPV), pp. 287–295.

FM-2006-UmenoL #automaton #case study #protocol #proving #safety #theorem proving #using

Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study (SU, NAL), pp. 64–80.

CAV-2006-Roe #heuristic #modulo theories #proving #smt #theorem proving

The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover (KR), pp. 467–470.

ASE-2005-WardKA #framework #named #proving #theorem proving

Prufrock: a framework for constructing polytypic theorem provers (JW, GK, PA), pp. 423–426.

TACAS-2005-IsobeR #csp #proving #refinement #theorem proving

A Generic Theorem Prover of CSP Refinement (YI, MR), pp. 108–123.

TACAS-2005-LeinoMO #proving #quantifier #theorem proving

A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover (KRML, MM, XO), pp. 334–348.

ICALP-2005-PersianoV #concurrent #constant

Single-Prover Concurrent Zero Knowledge in Almost Constant Rounds (GP, IV), pp. 228–240.

CADE-2005-ChaudhuriP #first-order #linear #logic #proving #theorem proving

A Focusing Inverse Method Theorem Prover for First-Order Linear Logic (KC, FP), pp. 69–83.

TACAS-2004-McMillan #proving #theorem proving

An Interpolating Theorem Prover (KLM), pp. 16–30.

IJCAR-2004-DenneyFS #automation #proving #theorem proving #using

Using Automated Theorem Provers to Certify Auto-generated Aerospace Software (ED, BF, JS), pp. 198–212.

IJCAR-2004-HustadtKRV #named #proving

TeMP: A Temporal Monodic Prover (UH, BK, AR, AV), pp. 326–330.

IJCAR-2004-WintersteinBG #diagrams #proving #theorem proving

Dr.Doodle: A Diagrammatic Theorem Prover (DW, AB, CAG), pp. 331–335.

FME-2003-MammarL #automation #database #design #proving #refinement

Design of an Automatic Prover Dedicated to the Refinement of Database Applications (AM, RL), pp. 834–854.

CADE-2003-HustadtK #proving

TRP++2.0: A Temporal Resolution Prover (UH, BK), pp. 274–278.

RTA-2003-Kutsia #equation #proving

Equational Prover of THEOREMA (TK), pp. 367–379.

STOC-2002-Khot02a #game studies #on the #power of

On the power of unique 2-prover 1-round games (SK), pp. 767–775.

LOPSTR-2002-Martin-MateosAHR #framework #verification

Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers (FJMM, JAA, MJH, JLRR), pp. 182–198.

ICALP-2001-GoldreichVW #interactive #on the #proving

On Interactive Proofs with a Laconic Prover (OG, SPV, AW), pp. 334–345.

CAV-2001-Bertot #formal method #proving #theorem proving #verification

Formalizing a JVML Verifier for Initialization in a Theorem Prover (YB), pp. 14–24.

IJCAR-2001-Beeson #higher-order #proving #theorem proving

A Second-Order Theorem Prover Applied to Circumscription (MB), pp. 318–324.

IJCAR-2001-CerroFGHLM #logic #proving

Lotrec : The Generic Tableau Prover for Modal and Description Logics (LFdC, DF, OG, AH, DL, FM), pp. 453–458.

IJCAR-2001-Happe #proving #theorem proving

The MODPROF Theorem Prover (JH), pp. 459–463.

IJCAR-2001-HodasT #agile #first-order #implementation #linear #logic #named #proving #theorem proving

lolliCop — A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic (JSH, NT), pp. 670–684.

IJCAR-2001-LetzS #calculus #named #proving #theorem proving

DCTP — A Disconnection Calculus Theorem Prover — System Abstract (RL, GS), pp. 381–385.

IJCAR-2001-Pastre #deduction #knowledge-based #proving #theorem proving

MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction (DP), pp. 685–689.

IJCAR-2001-SchmittLKN #interactive #proving #theorem proving

JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants (SS, LL, CK, AN), pp. 421–426.

TACAS-2000-MeyerP #architecture #interactive #proving

An Architecture for Interactive Program Provers (JM, APH), pp. 63–77.

STOC-2000-Vadhan #complexity #interactive #on the #proving

On transformation of interactive proofs that preserve the prover’s complexity (SPV), pp. 200–207.

CADE-2000-NeculaL #generative #proving #theorem proving

Proof Generation in the Touchstone Theorem Prover (GCN, PL), pp. 25–44.

CADE-2000-Sinz #algebra #automation #proving #theorem proving

System Description: ARA — An Automatic Theorem Prover for Relation Algebras (CS), pp. 177–182.

TACAS-1999-SpeltE #analysis #database #object-oriented #theorem proving

A Theorem Prover-Based Analysis Tool for Object-Oriented Databases (DS, SE), pp. 375–389.

CADE-1999-HutterB #contest #design #induction #proving #theorem proving

The Design of the CADE-16 Inductive Theorem Prover Contest (DH, AB), pp. 374–377.

CADE-1999-JanicicBG #flexibility #framework #integration #proving #theorem proving

A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers (PJ, AB, IG), pp. 127–141.

CADE-1999-Nipkow #programming language #proving #theorem proving

Invited Talk: Embedding Programming Languages in Theorem Provers (Abstract) (TN), p. 398.

CADE-1999-Voronkov #named #proving #theorem proving

KK: a theorem prover for K (AV), pp. 383–387.

ASE-1998-Ledru #identification #proving #theorem proving

Identifying Pre-Conditions with the Z/EVES Theorem Prover (YL), p. 32–?.

CSMR-1998-JakobiW #automation #database #evaluation #framework #maintenance #named #proving #theorem proving

DBFW: A Simple DataBase FrameWork for the Evaluation and Maintenance of Automated Theorem Prover Data (PJ, AW), pp. 185–188.

CADE-1998-BenzmullerK98a #higher-order #proving #theorem proving

System Description: LEO — A Higher-Order Theorem Prover (CB, MK), pp. 139–144.

CADE-1998-GorePSV #proving #smarttech #theorem proving

System Description: card TAP: The First Theorem Prover on a Smart Card (RG, JP, AS, HV), pp. 47–50.

CAV-1998-HardinWG #concept #design #proving #theorem proving

Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle (DSH, MW, DAG), pp. 39–44.

RTA-1998-Fuchs #information management #proving

Coupling Saturation-Based Provers by Exchanging Positive/Negative Information (DF), pp. 317–331.

TACAS-1997-SandnerM #proving #refinement #theorem proving

Theorem Prover Support for the Refinement of Stream Processing Functions (RS, OM), pp. 351–365.

CADE-1997-Bonacina #proving #theorem proving

The Clause-Diffusion Theorem Prover Peers-mcd (System Description) (MPB), pp. 53–56.

CADE-1997-FuchsF #named #problem #proving

CODE: A Powerful Prover for Problems of Condensed Detachment (DF, MF), pp. 260–263.

CADE-1997-Iwanuma #proving #theorem proving #top-down

Lemma Matching for a PTTP-based Top-down Theorem Prover (KI), pp. 146–160.

CADE-1997-KolbeB #learning #named #proving

Plagiator — A Learning Prover (TK, JB), pp. 256–259.

CADE-1997-LoweD #named #proving #theorem proving

XBarnacle: Making Theorem Provers More Accessible (HL, DD), pp. 404–407.

CADE-1997-Slaney #logic #named #proving #theorem proving

Minlog: A Minimal Logic Theorem Prover (JKS), pp. 268–271.

CADE-1997-Zhang #named #performance #proving

SATO: An Efficient Propositional Prover (HZ), pp. 272–275.

CADE-1996-BeckertHOS #proving #theorem proving

The Tableau-based Theorem Prover 3TAP Version 4.0 (BB, RH, PO, MS), pp. 303–307.

CADE-1996-SchaubBN #named #prolog #proving #reasoning #theorem proving

XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description (TS, SB, PN), pp. 293–297.

CADE-1996-Schumann #named #parallel #proving #theorem proving

SiCoTHEO: Simple Competitive Parallel Theorem Provers (JS), pp. 240–244.

CADE-1996-Tammet #logic #proving #theorem proving

A Resolution Theorem Prover for Intuitonistic Logic (TT), pp. 2–16.

CADE-1996-Wang #geometry #named #proving #theorem proving

GEOTHER: A Geometry Theorem Prover (DW), pp. 166–170.

RTA-1996-VandevoordeK #distributed #empirical #proving #rule-based

Distributed Larch Prover (DLP): An Experiment in Parallelizing a Rewrite-Rule Based Prover (MTV, DK), pp. 420–423.

RTA-1996-Voisin #interface #proving

A New Proof Manager and Graphic Interface for Larch Prover (FV), pp. 408–411.

STOC-1995-FeigeK #proving #random

Impossibility results for recycling random bits in two-prover proof systems (UF, JK), pp. 457–468.

ICLP-1995-FormicaMT #database #object-oriented #proving #satisfiability #theorem proving

A Theorem Prover for Checking Satisfiability of Object-Oriented Database Schemas (AF, MM, RT), p. 819.

ICLP-1995-Hasegawa #generative #proving #theorem proving

Model Generation Theorem Provers and Their Applications (RH), p. 7.

RTA-1995-Holmes #equation #proving #recursion #theorem

Disguising Recursively Chained Rewrite Rules as Equational Theorems, as Implemented in the Prover EFTTP Mark 2 (MRH), pp. 432–437.

STOC-1994-FeigeK #fault #protocol #proving

Two prover protocols: low error at affordable rates (UF, JK), pp. 172–183.

CADE-1994-Schumann #bottom-up #named #preprocessor #proving #theorem proving #top-down

DELTA — A Bottom-up Preprocessor for Top-Down Theorem Provers — System Abstract (JS), pp. 774–777.

STOC-1992-BellareP #performance #proving

Making Zero-Knowledge Provers Efficient (MB, EP), pp. 711–722.

STOC-1992-FeigeL92a #problem #proving

Two-Prover One-Round Proof Systems: Their Power and Their Problems (Extended Abstract) (UF, LL), pp. 733–744.

KR-1992-Lamarre #proving #theorem proving

A Promenade from Monotonicity to Non-Monotonicity Following a Theorem Prover (PL), pp. 572–580.

CADE-1992-AstrachanS #proving #theorem proving

Caching and Lemmaizing in Model Elimination Theorem Provers (OLA, MES), pp. 224–238.

CADE-1992-Baker-PlummerR #proving #theorem proving

The GAZER Theorem Prover (DBP, AR), pp. 726–730.

CADE-1992-BeckertGHK #logic #multi #proving #theorem proving

The Tableau-Based Theorem Prover 3TAP for Multi-Valued Logics (BB, SG, RH, WK), pp. 758–760.

CADE-1992-Chou #geometry #proving #theorem proving

A Geometry Theorem Prover for Macintoshes (SCC), pp. 686–690.

CADE-1992-ClarkeZ #named #proving #theorem proving

Analytica — A Theorem Prover in Mathematica (EMC, XZ), pp. 761–765.

CADE-1992-HasegawaKF #generative #lazy evaluation #named #parallel #proving #theorem proving

MGTP: A Parallel Theorem Prover Based on Lazy Model Generation (RH, MK, HF), pp. 776–780.

CADE-1992-InoueKH #generative #proving #theorem proving

Embedding Negation as Failure into a Model Generation Theorem Prover (KI, MK, RH), pp. 400–415.

CADE-1992-LuskMS #named #parallel #proving #theorem proving

ROO: A Parallel Theorem Prover (ELL, WM, JKS), pp. 731–734.

CADE-1992-RandellCC #automation #challenge #proving #theorem proving

Computing Transivity Tables: A Challenge For Automated Theorem Provers (DAR, AGC, ZC), pp. 786–790.

CADE-1992-SchneiderKK #proving

The FAUST — Prover (KS, RK, TK), pp. 766–770.

CADE-1992-Schumann #logic #named #proving #theorem proving

KPROP — An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract) (JS), pp. 740–742.

CAV-1992-WrightL #algorithm #concurrent #proving #reasoning #theorem proving #using

Using a Theorem Prover for Reasoning about Concurrent Algorithms (JvW, TL), pp. 56–68.

PLILP-1991-FrausH #proving #theorem proving

A Narrowing-Based Theorem Prover (UF, HH), pp. 421–422.

ICLP-1991-FujitaH #algorithm #generative #proving #theorem proving #using

A Model Generation Theorem Prover in KL1 Using a Ramified -Stack Algorithm (HF, RH), pp. 535–548.

RTA-1991-Deruyver #equation #first-order #logic #named #proving #theorem proving

EMMY: A Refutational Theorem Prover for First-Order Logic with Equation (AD), pp. 439–441.

RTA-1991-Fraus #proving #theorem proving

A Narrowing-Based Theorem Prover (UF), pp. 435–436.

ICSE-1990-LafontaineLS #case study #development #empirical #formal method #proving #theorem proving #using

An Experiment in Formal Software Development: Using the B Theorem Prover on a VDM Case Study (CL, YL, PYS), pp. 34–42.

CADE-1990-BoyerM #logic #proving #theorem proving

A Theorem Prover for a Computational Logic (RSB, JSM), pp. 1–15.

CADE-1990-ButlerFJO #parallel #proving #theorem proving

A High-Performance Parallel Theorem Prover (RB, ITF, AJ, RAO), pp. 649–650.

CADE-1990-Gramlich #induction #named #proving #theorem proving

UNICOM: A Refined Completion Based Inductive Theorem Prover (BG), pp. 655–656.

CADE-1990-Hines #proving #set

Str+ve-Subset: The Str+ve-based Subset Prover (LMH), pp. 193–206.

CADE-1990-KaflZ #proving #theorem proving #verification

The Theorem Prover of the Program Verifier Tatzelwurm (TK, NZ), pp. 657–658.

CADE-1990-MurrayR #named #proving #theorem proving

DISSOLVER: A Dissolution-based Theorem Prover (NVM, ER), pp. 665–666.

CADE-1990-SchumannL #named #parallel #proving #theorem proving

PARTHEO: A High-Performance Parallel Theorem Prover (JS, RL), pp. 40–56.

CADE-1990-SchumannLK #implementation #parallel #performance #proving #theorem proving #tutorial

Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation (JS, RL, FJK), p. 683.

CADE-1990-Schwind #decidability #logic #proving #set #theorem proving

A Tableau-Based Theorem Prover for a Decidable Subset of Default Logic (CS), pp. 528–542.

CADE-1990-Stickel #prolog #proving #theorem proving

A Prolog Technology Theorem Prover (MES), pp. 673–674.

CADE-1990-Sutcliffe #proving #theorem proving

A General Clause Theorem Prover (GS), pp. 675–676.

CADE-1990-Tarver #prolog

An Examination of the Prolog Technology Theorem-Prover (MT), pp. 322–335.

CSL-1990-HertrampfW #bound #fault #interactive #proving

Interactive Proof Systems: Provers, Rounds, and Error Bounds (UH, KWW), pp. 261–273.

LICS-1989-BoseCLM #horn clause #named #parallel #proving #theorem proving

PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (SB, EMC, DEL, SM), pp. 80–89.

RTA-1989-AvenhausDM #named #performance #proving #theorem proving

THEOPOGLES — An efficient Theorem Prover based on Rewrite-Techniques (JA, JD, JM), pp. 538–541.

RTA-1989-BonacinaS #equation #named #proving #theorem proving

KBlab: An Equational Theorem Prover for the Macintosh (MPB, GS), pp. 548–550.

SIGMOD-1988-MazumdarSS #proving #security #theorem proving #using

Resolving the Tension between Integrity and Security Using a Theorem Prover (SM, DWS, TS), pp. 233–242.

STOC-1988-Ben-OrGKW #how #interactive #multi #proving

Multi-Prover Interactive Proofs: How to Remove Intractability Assumptions (MBO, SG, JK, AW), pp. 113–131.

CADE-1988-AllenBCM #horn clause #named #parallel #proving #theorem proving

PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (PEA, SB, EMC, SM), pp. 764–765.

CADE-1988-BrownP #logic #named #proving #theorem proving

SYMEVAL: A Theorem Prover Based on the Experimental Logic (FMB, SSP), pp. 756–757.

CADE-1988-CyrlukHK #algebra #geometry #named #proving #theorem proving

GEOMETER: A Theorem Prover for Algebraic Geometry (DC, RMH, DK), pp. 770–771.

CADE-1988-FeltyM #higher-order #logic programming #programming language #proving #specification #theorem proving

Specifying Theorem Provers in a Higher-Order Logic Programming Language (APF, DM), pp. 61–80.

CADE-1988-GarlandG #named #proving

LP: The Larch Prover (SJG, JVG), pp. 748–749.

CADE-1988-Kaufmann #interactive #proving #theorem proving

An Interactive Enhancement to the Boyer-Moore Theorem Prover (MK), pp. 735–736.

CADE-1988-MantheyB #named #prolog #proving #theorem proving

SATCHMO: A Theorem Prover Implemented in Prolog (RM, FB), pp. 415–434.

CADE-1988-Paulson #named #proving #theorem proving

Isabelle: The Next Seven Hundred Theorem Provers (LCP), pp. 772–773.

CADE-1988-Plaisted #proving #theorem proving

A Goal Directed Theorem Prover (DAP), p. 737.

CADE-1988-Stevens #challenge #problem #proving #theorem proving

Challenge Problems from Nonassociative Rings for Theorem Provers (RLS), pp. 730–734.

CADE-1988-Stickel88a #prolog #proving #theorem proving

A Prolog Technology Theorem Prover (MES), pp. 752–753.

CADE-1986-BoyerM #bibliography #logic

Overview of a Theorem-Prover for A Computational Logic (RSB, JSM), pp. 675–678.

CADE-1986-Chou #geometry #named #proving #theorem proving

GEO-Prover — A Geometry Theorem Prover Developed at UT (SCC), pp. 679–680.

CADE-1986-GreenbaumP #proving #theorem proving

The Illinois Prover: A General Purpose Resolution Theorem Prover (SG, DAP), pp. 685–687.

CADE-1986-KutzlerS #algorithm #geometry #proving #theorem proving

A Geometry Theorem Prover Based on Buchberger’s Algorithm (BK, SS), pp. 693–694.

CADE-1986-Stickel #compilation #implementation #prolog #proving #theorem proving

A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler (MES), pp. 573–587.

CADE-1986-Wang86a

SHD-Prover at University of Texas at Austin (TCW), pp. 707–708.

CADE-1984-OhlbachW #automation #logic #problem #proving #theorem proving

Solving a Problem in Relevance Logic with an Automated Theorem Prover (HJO, GW), pp. 496–508.

CADE-1984-Suppes #generative #interactive #proving #theorem proving

The Next Generation of Interactive Theorem Provers (PS), pp. 303–315.

SLP-1984-Stickel84 #prolog #proving #theorem proving

A Prolog Technology Theorem Prover (MES), pp. 211–217.

CADE-1980-BledsoeH #proving

Variable Elimination and Chaining in a Resolution-based Prover for Inequalities (WWB, LMH), pp. 70–87.

CADE-1980-EricksonM #proving #scalability #theorem proving

The AFFIRM Theorem Prover: Proof Forests and Management of Large Proofs (RWE, DRM), pp. 220–231.

CADE-1980-Gloess #correctness #empirical #parsing #proving #theorem proving

An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions (PYG), pp. 154–169.

STOC-1970-KingF #integer #proving #theorem proving

An Interpretation Oriented Theorem Prover over Integers (JCK, RWF), pp. 169–179.