Harald Ganzinger
Proceedings of the Seventh International Conference on Rewriting Techniques and Applications
RTA, 1996.

@proceedings{RTA-1996,
	address       = "New Brunswick, New Jersey, USA",
	editor        = "Harald Ganzinger",
	isbn          = "3-540-61464-8",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Seventh International Conference on Rewriting Techniques and Applications}",
	volume        = 1103,
	year          = 1996,
}

Contents (37 items)

10 ×#proving
7 ×#higher-order
5 ×#term rewriting
4 ×#on the
4 ×#termination
4 ×#unification
3 ×#named
3 ×#theorem proving
2 ×#composition
2 ×#confluence

RTA-1996-Kapur #automation #challenge #reasoning

Rewrite-Based Automated Reasoning: Challenges Ahead (DK), pp. 1–2.

RTA-1996-KirchnerLS #concurrent #fine-grained

Fine-Grained Concurrent Completion (CK, CL, CS), pp. 3–17.

RTA-1996-BoudetCM #proving #theorem proving #unification

AC-Complete Unification and its Application to Theorem Proving (AB, EC, CM), pp. 18–32.

RTA-1996-Stuber #integer #proving #theorem proving

Superposition Theorem Proving for Albelian Groups Represented as Integer Modules (JS), pp. 33–47.

RTA-1996-Gobel

Symideal Gröbner Bases (MG), pp. 48–62.

RTA-1996-ArtsG #termination

Termination of Constructor Systems (TA, JG), pp. 63–77.

RTA-1996-Ferreira #equation

Dummy Elimination in Equational Rewriting (MCFF), pp. 78–92.

RTA-1996-Gramlich #on the #proving #termination

On Proving Termination by Innermost Termination (BG), pp. 93–107.

RTA-1996-JouannaudR #higher-order #normalisation #recursion

A Recursive Path Ordering for Higher-Order Terms in η-Long β-Normal Form (JPJ, AR), pp. 108–122.

RTA-1996-Virga #dependent type #higher-order

Higher-Order Superposition for Dependent Types (RV), pp. 123–137.

RTA-1996-HanusP #higher-order

Higher-Order Narrowing with Definitional Trees (MH, CP), pp. 138–152.

RTA-1996-Huet #design #proving

Design Proof Assistant (GPH), p. 153.

RTA-1996-Vittek #compilation #nondeterminism #term rewriting

A Compiler for Nondeterministic Term Rewriting Systems (MV), pp. 154–167.

RTA-1996-BlooR #combinator #reduction

Combinatory Reduction Systems with Explicit Substitution that Preserve Strong Nomalisation (RB, KHR), pp. 169–183.

RTA-1996-Kesner #confluence #λ-calculus

Confluence Properties of Extensional and Non-Extensional λ-Calculi with Explicit Substitutions (DK), pp. 184–199.

RTA-1996-Cosmo #diagrams #on the #power of

On the Power of Simple Diagrams (RDC), pp. 200–214.

RTA-1996-GuerriniMM #proving

Coherence for Sharing Proof Nets (SG, SM, AM), pp. 215–229.

RTA-1996-Rao #composition #graph grammar #termination

Modularity of Termination in Term Graph Rewriting (MRKKR), pp. 230–244.

RTA-1996-GramlichW #confluence #revisited #term rewriting

Confluence of Terminating Conditional Rewrite Systems Revisited (BG, CPW), pp. 245–259.

RTA-1996-Madlener #monad

Applications of Rewrite Techniques in Monoids and Rings (KM), p. 260.

RTA-1996-Luth #algebra #composition #proving #term rewriting #theorem

Compositional Term Rewriting: An Algebraic Proof of Toyama’s Theorem (CL), pp. 261–275.

RTA-1996-Treinen #decidability #first-order

The First-Order Theory of One-Step Rewriting is Undecidable (RT), pp. 276–286.

RTA-1996-Schmidt-Schauss #algorithm #unification

An Algorithm for Distributive Unification (MSS), pp. 287–301.

RTA-1996-Senizergues #on the #problem #termination

On the Termination Problem for One-Rule Semi-Thue System (GS), pp. 302–316.

RTA-1996-CurienQS #higher-order #performance

Efficient Second-Order Matching (RC, ZQ, HS), pp. 317–331.

RTA-1996-Levy #higher-order #linear #unification

Linear Second-Order Unification (JL), pp. 332–346.

RTA-1996-FettigL #finite #higher-order #unification #λ-calculus

Unification of Higher-Order patterns in a Simply Typed λ-Calculus with Finite Products and terminal Type (RF, BL), pp. 347–361.

RTA-1996-Jacquemard #approximate #decidability #term rewriting

Decidable Approximations of Term Rewriting Systems (FJ), pp. 362–376.

RTA-1996-SakaiT #semantics #term rewriting

Semantics and Strong Sequentiality of Priority Term Rewriting Systems (MS, YT), pp. 377–391.

RTA-1996-Oostrom #higher-order #product line

Higher-Order Families (VvO), pp. 392–407.

RTA-1996-Voisin #interface #proving

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

RTA-1996-BundgenSW

ReDuX 1.5: New Facets of Rewriting (RB, CS, JW), pp. 412–415.

RTA-1996-ContejeanM #named

CiME: Completion Modulo E (EC, CM), pp. 416–419.

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-WaltersK #automaton #equation #named

EPIC: An Equational Language -Abstract Machine Supporting Tools- (HRW, JFTK), pp. 424–427.

RTA-1996-BerregebBR #commutative #induction #named #proving

SPIKE-AC: A System for Proofs by Induction in Associative-Commutative Theories (NB, AB, MR), pp. 428–431.

RTA-1996-HillenbrandBF #on the #performance #proving #theorem proving

On Gaining Efficiency in Completion-Based Theorem Proving (TH, AB, RF), pp. 432–435.