Regular Patterns in Second-Order Unification

DOI10.1007/978-3-319-21401-6_38zbMath1465.03054OpenAlexW1424724424MaRDI QIDQ3454122

Tomer Libal

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_38

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items (3)

Unnamed Item ⋮ Superposition with lambdas ⋮ Superposition with lambdas

Uses Software

• TPS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Decreasing diagrams and relative termination
• Reasoning about sequences of memory states
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A unification algorithm for second-order monadic terms
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Higher-order unification revisited: Complete sets of transformations
• Decidability of bounded higher-order unification
• Minimal and complete word unification
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Towards parametrizing word equations
• On the Velocity-Pressure-Vorticity Least-Squares Mixed Finite Element Method for the 3D Stokes Equations
• A Decision Algorithm for Stratified Context Unification
• Linear second-order unification
• Decidable higher-order unification problems

This page was built for publication: Regular Patterns in Second-Order Unification