Massive unification

DOI10.1016/J.JLAMP.2026.101147MaRDI QIDQ7320668zbMATH OpenFDO

Authors Javier Álvez, A. Perez, M. Hermo, José A. Pascual

Publication date 27 August 2026

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JLAMP.2026.101147

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
• A Machine-Oriented Logic Based on the Resolution Principle
• An almost linear Robinson unification algorithm
• An Efficient Unification Algorithm
• Equational problems and disunification
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Extracting models from clause sets saturated under semantic refinements of the resolution rule.
• Linear unification
• On the sequential nature of unification
• OpenSMT2: an SMT solver for multi-core and cloud computing
• Parallel Logic Programming: A Sequel
• Term indexing
• The anatomy of vampire. Implementing bottom-up procedures with code trees
• The higher-order prover Leo-III
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0

This page was built for publication: Massive unification

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