Higher-order pattern generalization modulo equational theories

DOI10.1017/S0960129520000110zbMath1495.03013OpenAlexW3026831509MaRDI QIDQ5139277

Temur Kutsia, David M. Cerna

Publication date: 8 December 2020

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129520000110

zbMATH Keywords

equational theoriessimply typed lambda calculusanti-unificationhigher-order patterns

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Uses Software

• ACUOS2

Cites Work

• Unnamed Item
• Unnamed Item
• Algorithmic introduction of quantified cuts
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Inductive synthesis of functional programs. Universal planning, folding of finite programs, and schema abstraction by analogical reasoning.
• \({\mathsf{ACUOS}}^\mathbf{2}\): a high-performance system for modular ACU generalization with subtyping and inheritance
• Inductive theorem proving based on tree grammars
• Anti-unification for unranked terms and hedges
• Higher-order pattern anti-unification in linear time
• Unranked second-order anti-unification
• On the generation of quantified lemmas
• A modular order-sorted equational generalization algorithm
• A Library of Anti-unification Algorithms
• Higher-order term indexing using substitution trees
• A Variant of Higher-Order Anti-Unification
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Algorithmic Compression of Finite Tree Languages by Rigid Acyclic Grammars
• Idempotent Anti-unification
• A Generic Framework for Higher-Order Generalizations.
• Heuristic-Driven Theory Projection: An Overview

This page was built for publication: Higher-order pattern generalization modulo equational theories