Higher-order pattern generalization modulo equational theories

DOI10.1017/S0960129520000110MaRDI QIDQ5139277zbMATH OpenOpenAlexFDO

Authors David M. Cerna, Temur Kutsia

Publication date 8 December 2020

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

anti-unificationequational theorieshigher-order patternssimply typed lambda calculus

Mathematics Subject Classification ID

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

Recommendations

• Higher-order equational pattern anti-unification
• Higher-order pattern anti-unification in linear time
• A variant of higher-order anti-unification
• A modular order-sorted equational generalization algorithm
• Nominal anti-unification

Cites work

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

Cited in

(17)

• Order-sorted equational generalization algorithm revisited
• Higher-order pattern anti-unification in linear time
• A modular order-sorted equational generalization algorithm
• ACUOS: a system for modular ACU generalization with subtyping and inheritance
• A variant of higher-order anti-unification
• Anti-pattern Matching Modulo
• A Modular Equational Generalization Algorithm
• scientific article; zbMATH DE number 914131 (Why is no real title available?)
• scientific article; zbMATH DE number 1447313 (Why is no real title available?)
• Idempotent anti-unification
• Higher-order equational pattern anti-unification
• A Generic Framework for Higher-Order Generalizations.
• One or nothing: anti-unification over the simply-typed lambda calculus
• Nominal anti-unification modulo equational theories
• Unital anti-unification: type and algorithms
• Equational generalization problems with atom-variables
• Anti-patterns for rule-based languages

Describes a project that uses

Uses Software

• ACUOS2

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5139277)