William McCune
Proceedings of the 14th International Conference on Automated Deduction
CADE, 1997.

@proceedings{CADE-1997,
	address       = "North Queensland, Australia",
	editor        = "William McCune",
	isbn          = "3-540-63104-6",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 14th International Conference on Automated Deduction}",
	volume        = 1249,
	year          = 1997,
}

Contents (44 items)

17 ×#proving
13 ×#named
7 ×#logic
7 ×#theorem proving
4 ×#automation
3 ×#using
2 ×#algorithm
2 ×#constraints
2 ×#implementation
2 ×#induction

CADE-1997-Wen-Tsun #automation #reasoning

The Char-Set Method and Its Applications to Automated Reasoning (WWT), pp. 1–3.

CADE-1997-DurandM #call-by #decidability #term rewriting

Decidable Call by Need Computations in term Rewriting (ID, AM), pp. 4–18.

CADE-1997-BaaderT #approach #problem #word

A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method (FB, CT), pp. 19–33.

CADE-1997-NiehrenPR #constraints #finite #on the #similarity #unification

On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting (JN, MP, PR), pp. 34–48.

CADE-1997-NieuwenhuisRV #algorithm #automation #data type #deduction #kernel #named #similarity

Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses (RN, JMR, MÁV), pp. 49–52.

CADE-1997-Bonacina #proving #theorem proving

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

CADE-1997-DahnGHW #automation #integration #interactive #proving #theorem proving

Integration of Automated and Interactive Theorem Proving in ILP (BID, JG, TH, AW), pp. 57–60.

CADE-1997-WolfS #named #natural language #proving

ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output (AW, JS), pp. 61–64.

CADE-1997-FischerS #re-engineering #reuse

SETHEO Goes Software Engineering: Application of ATP to Software Reuse (BF, JS), pp. 65–68.

CADE-1997-ReifSS #correctness #proving

Proving System Correctness with KIV 3.0 (WR, GS, KS), pp. 69–72.

CADE-1997-YangFZ #algorithm #geometry

A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple Geometry (LY, HF, ZZ), pp. 73–86.

CADE-1997-Schumann #automation #encryption #protocol #verification

Automatic Verification of Cryptographic Protocols with SETHEO (JS), pp. 87–100.

CADE-1997-BjornerSU #first-order #integration #reasoning

A Practical Integration of First-Order Reasoning and Decision Procedures (NB, MES, TEU), pp. 101–115.

CADE-1997-Egly #how

Some Pitfalls of LK-to-LJ Translations and How to Avoid Them (UE), pp. 116–130.

CADE-1997-KornK #logic

Deciding Intuitionistic Propositional Logic via Translation into Classical Logic (DSK, CK), pp. 131–145.

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

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

CADE-1997-RousselM #calculus #compilation

Exact Kanowledge Compilation in Predicate Calculus: The Partial Achievement Case (OR, PM), pp. 161–175.

CADE-1997-HasegawaIOK #bottom-up #proving #set #theorem proving #top-down

Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving (RH, KI, YO, MK), pp. 176–190.

CADE-1997-Vardi #automaton #logic

Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics (MYV), pp. 191–206.

CADE-1997-KreitzMOS #linear #logic #proving

Connection-Based Proof Construction in Linear Logic (CK, HM, JO, SS), pp. 207–221.

CADE-1997-HarlandP #constraints

Resource-Distribution via Boolean Constraint (JH, DJP), pp. 222–236.

CADE-1997-CryanR #normalisation

Constructing a Normal Form for Property Theory (MC, AR), pp. 237–251.

CADE-1997-BenzmullerCFFHKKKMMSSS #named #towards

Omega: Towards a Mathematical Assistant (CB, LC, DF, AF, XH, MK, MK, KK, AM, EM, WS, JHS, VS), pp. 252–255.

CADE-1997-KolbeB #learning #named #proving

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

CADE-1997-FuchsF #named #problem #proving

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

CADE-1997-GiunchigliaRS #logic #testing

A New Method for Testing Decision Procedures in Modal Logics (FG, MR, RS), pp. 264–267.

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-1997-DennisBG #bisimulation #induction #proving #using

Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs (LAD, AB, IG), pp. 276–290.

CADE-1997-HutterK #λ-calculus

A Colored Version of the Lambda-Calculus (DH, MK), pp. 291–305.

CADE-1997-Matthews #implementation #induction #using

A Practical Implementation of Simple Consequence Relations Using Inductive Definitions (SM), pp. 306–320.

CADE-1997-GanzingerMW #order #type system

Soft Typing for Ordered Resolution (HG, CM, CW), pp. 321–335.

CADE-1997-Nivelle #classification #order

A Classification of Non-liftable Orders for Resolution (HdN), pp. 336–350.

CADE-1997-FeltyH #hybrid #interactive #proving #theorem proving #using

Hybrid Interactive Theorem Proving Using Nuprl and HOL (APF, DJH), pp. 351–365.

CADE-1997-EastaughffeOC #formal method #proving #state machine #visual notation

Proof Tactics for a Theory of State Machines in a Graphical Environment (KAE, MAO, AC), pp. 366–379.

CADE-1997-OheimbG #algebra #named #proving

RALL: Machine-Supported Proofs for Relation Algebra (DvO, TFG), pp. 380–394.

CADE-1997-Hickey #framework #higher-order #implementation #logic #named

Nuprl-Light: An Implementation Framework for Higher-Order Logics (JJH), pp. 395–399.

CADE-1997-OzolsCE #named

XIsabelle: A System Description (MAO, AC, KAE), pp. 400–403.

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

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

CADE-1997-KettnerE

The Tableau Browser SNARKS (MK, NE), pp. 408–411.

CADE-1997-BornatS #named

Jape: A Calculator for Animating Proof-on-Paper (RB, BS), pp. 412–415.

CADE-1997-Fuchs #combinator #evolution

Evolving Combinators (MF), pp. 416–430.

CADE-1997-DefourneauxP #proving

Partial Matching for Analogy Discovery in Proofs and Counter-Examples (GD, NP), pp. 431–445.

CADE-1997-EhrensbergerZ #logic #named

DiaLog: A System for Dialogue Logic (JE, CZ), pp. 446–460.