Mark E. Stickel
Proceedings of the 10th International Conference on Automated Deduction
CADE, 1990.

@proceedings{CADE-1990,
	editor        = "Mark E. Stickel",
	isbn          = "3-540-52885-7",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 10th International Conference on Automated Deduction}",
	volume        = 449,
	year          = 1990,
}

Contents (74 items)

26 ×#proving
17 ×#theorem proving
10 ×#named
9 ×#tutorial
8 ×#logic
7 ×#automation
5 ×#deduction
5 ×#equation
5 ×#set
5 ×#unification

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

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

CADE-1990-NieP #proving #semantics

A Complete Semantic Back Chaining Proof System (XN, DAP), pp. 16–27.

CADE-1990-SlaneyL #automation #deduction

Parallelizing the Closure Computation in Automated Deduction (JKS, ELL), pp. 28–39.

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

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

CADE-1990-LeeH #compilation #database #deduction

Substitution-based Compilation of Extended Rules in Deductive Databases (SHL, LJH), pp. 57–71.

CADE-1990-CostaHLS #automation #implementation #logic #proving #theorem proving

Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation (NCAdC, LJH, JJL, VSS), pp. 72–86.

CADE-1990-WakayamaP #abstraction #source code

Case-Free Programs: An Abstraction of Definite Horn Programs (TW, THP), pp. 87–101.

CADE-1990-BaralLM #logic programming #semantics #source code

Generalized Well-founded Semantics for Logic Programs (CB, JL, JM), pp. 102–116.

CADE-1990-HeiselRS #proving #theorem proving #verification

Tactical Theorem Proving in Program Verification (MH, WR, WS), pp. 117–131.

CADE-1990-BundyHSI #induction #proving

Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs (AB, FvH, AS, AI), pp. 132–146.

CADE-1990-Hutter #induction #proving

Guiding Induction Proofs (DH), pp. 147–161.

CADE-1990-Reddy #induction #term rewriting

Term Rewriting Induction (USR), pp. 162–177.

CADE-1990-Burckert #constraints

A Resolution Principle for Clauses with Constraints (HJB), pp. 178–192.

CADE-1990-Hines #proving #set

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

CADE-1990-ChouG #algorithm #composition #geometry #proving #theorem proving

Ritt-Wu’s Decomposition Algorithm and Geometry Theorem Proving (SCC, XSG), pp. 207–220.

CADE-1990-FeltyM #encoding #logic programming #programming language #λ-calculus

Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language (APF, DM), pp. 221–235.

CADE-1990-PymW #first-order

Investigations into Proof-Search in a System of First-Order Dependent Function Types (DJP, LAW), pp. 236–250.

CADE-1990-Basin #commutative #morphism #similarity

Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism Complete (DAB), pp. 251–260.

CADE-1990-DoughertyJ

An Improved General E-Unification Method (DJD, PJ), pp. 261–275.

CADE-1990-NarendranO #equation #unification

Some Results on Equational Unification (PN, FO), pp. 276–291.

CADE-1990-Boudet #algorithm #equation #performance #unification

Unification in a Combination of Equational Theories: an Efficient Algorithm (AB), pp. 292–307.

CADE-1990-McMichael #automation #named #set

SLIM: An Automated Reasoner For Equivalences, Applied To Set Theory (AFM), pp. 308–321.

CADE-1990-Tarver #prolog

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

CADE-1990-PfenningN #deduction #symmetry

Presenting Intuitive Deductions via Symmetric Simplification (FP, DN), pp. 336–350.

CADE-1990-Pierce #proving #towards

Toward Mechanical Methods for Streamlining Proofs (WP), pp. 351–365.

CADE-1990-MartinN #confluence #order

Ordered Rewriting and Confluence (UM, TN), pp. 366–380.

CADE-1990-Peterson #constraints #reduction #set

Complete Sets of Reductions with Constraints (GEP), pp. 381–395.

CADE-1990-Baader #term rewriting

Rewrite Systems for Varieties of Semigroups (FB), pp. 396–410.

CADE-1990-Steinbach #order

Improving Assoviative Path Orderings (JS), pp. 411–425.

CADE-1990-Bibel #automation #deduction

Perspectives on Automated Deduction (WB), p. 426.

CADE-1990-BachmairG #on the #order #strict

On Restrictions of Ordered Paramodulation with Simplification (LB, HG), pp. 427–441.

CADE-1990-Benanav

Simultaneous Paramodulation (DB), pp. 442–455.

CADE-1990-OzturkH #axiom #similarity

Hyper Resolution and Equality Axioms without Function Substitutions (YO, LJH), pp. 456–469.

CADE-1990-SuttnerE #automation #heuristic

Automatic Acquisition of Search Guiding Heuristics (CBS, WE), pp. 470–484.

CADE-1990-WosWMOLSB #automation #logic #reasoning

Automated Reasoning Contributed to Mathematics and Logic (LW, SW, WM, RAO, ELL, RLS, RB), pp. 485–499.

CADE-1990-AltucherP #category theory #proving

A Mechanically Assisted Constructive Proof in Category Theory (JAA, PP), pp. 500–513.

CADE-1990-Tuominen #framework #logic #proving #theorem proving

Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic (HT), pp. 514–527.

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-JacksonP

Computing Prime Implicants (PJ, JP), pp. 543–557.

CADE-1990-Tour

Minimizing the Number of Clauses by Renaming (TBdlT), pp. 558–572.

CADE-1990-Snyder #higher-order

Higher Order E-Unification (WS), pp. 573–587.

CADE-1990-Hagiya #higher-order #programming #proving #unification #using

Programming by Example and Proving by Example Using Higher-order Unification (MH), pp. 588–602.

CADE-1990-Rittri #equation #identifier #library

Retrieving Library Identifiers via Equational Matching of Types (MR), pp. 603–617.

CADE-1990-Nutt #unification

Unification in Monoidal Theories (WN), pp. 618–632.

CADE-1990-Bundy #reasoning

A Science of Reasoning: Extended Abstract (AB), pp. 633–640.

CADE-1990-AndrewsINP #proving #theorem proving

The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 641–642.

CADE-1990-BrownA

Schemata (FMB, CA), pp. 643–644.

CADE-1990-BrownA90a #algebra #equation

Cylindric Algebra Equation Solver (FMB, CA), pp. 645–646.

CADE-1990-BundyHHS

The Oyster-Clam System (AB, FvH, CH, AS), pp. 647–648.

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

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

CADE-1990-EichenlaubEHKP #proving

The Romulus Proof Checker (CE, BE, JH, CK, GP), pp. 651–652.

CADE-1990-FarmerGT #interactive #named #proving

IMPS: An Interactive Mathematical Proof System (WMF, JDG, FJT), pp. 653–654.

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

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

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

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

CADE-1990-Kaufmann #lisp #named #verification

RCL: A Lisp Verification System (MK), pp. 659–660.

CADE-1990-Lescanne #implementation #named #set

ORME: An Implementation of Completion Procedures as Sets of Transition Rules (PL), pp. 661–662.

CADE-1990-McCune

OTTER 2.0 (WM), pp. 663–664.

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

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

CADE-1990-NieuwenhuisOR #implementation #named

TRIP: An Implementation of Clausal Rewriting (RN, FO, AR), pp. 667–668.

CADE-1990-Pollock

OSCAR (JLP), pp. 669–670.

CADE-1990-Satz #adaptation #prolog

EXPERT THINKER: An Adaptation of F-Prolog to Microcomputers (RWS), pp. 671–672.

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-Voronkov #logic #named

LISS — The Logic Inference Search System (AV), pp. 677–678.

CADE-1990-Wolfram #named

ACE: The Abstract Clause Engine (DAW), pp. 679–680.

CADE-1990-LuskM #automation #proving #theorem proving #tutorial

Tutorial on High-Performance Automated Theorem Proving (ELL, WM), p. 681.

CADE-1990-MullerBNNS #concept #reasoning #representation #tutorial

Tutorial on Reasoning and Representation with Concept Languages (JM, FB, BN, WN, GS), p. 681.

CADE-1990-FeltyGMP #prolog #tutorial #λ-calculus

Tutorial on Lambda-Prolog (APF, ELG, DM, FP), p. 682.

CADE-1990-Kirchner #equation #tutorial #unification

Tutorial on Equational Unification (CK), p. 682.

CADE-1990-OhlbachH #compilation #logic #tutorial

Tutorial on Compilation techniques for Logics (HJO, AH), p. 683.

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-HsiangJ #proving #theorem proving #tutorial

Tutorial on Rewrite-Based Theorem Proving (JH, JPJ), p. 684.

CADE-1990-Waldinger #deduction #tutorial

Tutorial on Program-Synthetic Deduction (RJW), p. 684.

CADE-1990-PritchardS #logic #modelling #tutorial

Tutorial on Computing Models of Propositional Logics (PP, JKS), p. 685.