Semantic Labelling in Practice
2026-07-01 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors studied ways to automate semantic labeling in termination proofs, a task that is very complex because there are many possible algebras to check. They experimented with their tools, Matchbox and MnM, to see how well different strategies work for finding models. These strategies included exhaustively checking small domains and using a method called semantic context-closure on fixed algebras. Their work compares these approaches to understand their effectiveness in handling this hard problem.
termination proofssemantic labelingalgebrasmodel findingexhaustive enumerationbounded domainsemantic context-closureMatchboxMnM
Authors
Dieter Hofbauer, Johannes Waldmann
Abstract
Automating semantic labelling for termination proofs is a combinatorially hard problem since the number of algebras grows prohibitively large even for small domains. We report on experiments with our tools Matchbox and MnM, comparing various model finding strategies: exhaustive enumeration for bounded domain sizes within restricted search spaces, and semantic context-closure for fixed algebras.