Proceedings of the 14th International Conference on Automated Deduction
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

TEST
DBLP
Scholar
Full names Links ISxN
@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)

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.

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.