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

Grammars and rewriting systems (68Q42) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) 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

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

Cited in

(11)

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

Describes a project that uses

Uses Software

• NQTHM
• Isabelle

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)