Efficient second-order matching

DOI10.1007/3-540-61464-8_62MaRDI QIDQ5055870zbMATH OpenOpenAlexFDO

Authors Régis Curien, Zhenyu Qian, Hui Shi

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61464-8_62

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Logic for Programming, Artificial Intelligence, and Reasoning
• Tractable and intractable second-order matching problems
• Publication:4938678
• Deterministic second-order patterns
• scientific article; zbMATH DE number 176135

Cites work

• A unification algorithm for typed -calculus
• Higher order E-unification
• Higher-order unification revisited: Complete sets of transformations
• scientific article; zbMATH DE number 4164171 (Why is no real title available?)
• scientific article; zbMATH DE number 176135 (Why is no real title available?)
• Isabelle. A generic theorem prover
• Modular higher-order E-unification
• Proving and applying program transformations expressed with second-order patterns

Cited in

(12)

• Deterministic second-order patterns
• Tractable and intractable second-order matching problems
• scientific article; zbMATH DE number 176135 (Why is no real title available?)
• scientific article; zbMATH DE number 1114050 (Why is no real title available?)
• Partial matching for analogy discovery in proofs and counter-examples
• Building proofs or counterexamples by analogy in a resolution framework
• Matching Modulo Superdevelopments Application to Second-Order Matching
• Second-Order Behavior of Pattern Search
• Inductive Logic Programming
• Logic for Programming, Artificial Intelligence, and Reasoning
• Analogy in automated deduction: a survey
• Higher-order matching for program transformation

Describes a project that uses

Uses Software

• Isabelle
• NQTHM

This page was built for publication: Efficient second-order matching

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