scientific article; zbMATH DE number 7471678

MaRDI QIDQ5028439

Visa Nummelin, Alexander Bentkamp, Petar Vukmirović

Publication date: 9 February 2022

Full work available at URL: https://arxiv.org/abs/2011.09507

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

theorem provinghigher-order logicunificationterm rewritingindexing data structures

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items (4)

Improving automation for higher-order proof steps ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ Making higher-order superposition work ⋮ A combinator-based superposition calculus for higher-order logic

Uses Software

• VAMPIRE
• TPTP
• Satallax
• StarExec
• Zipperposition

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A unification algorithm for second-order monadic terms
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• Isabelle/HOL. A proof assistant for higher-order logic
• Superposition with structural induction
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• The higher-order prover Leo-III
• Higher-order unification revisited: Complete sets of transformations
• LEO-II and Satallax on the Sledgehammer test bench
• Restricted combinatory unification
• Higher-order unification via combinators
• Programming with Higher-Order Logic
• Satallax: An Automatic Higher-Order Prover
• Fingerprint Indexing for Paramodulation and Rewriting
• Regular Patterns in Second-Order Unification
• Proving termination with multiset orderings
• The CADE-27 Automated theorem proving System Competition – CASC-27
• Functions-as-constructors Higher-order Unification
• A Machine-Oriented Logic Based on the Resolution Principle

This page was built for publication: