Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915713071972352 |
|---|---|
| author | Yang, Ziyi Pîrlea, George Sergey, Ilya |
| author_facet | Yang, Ziyi Pîrlea, George Sergey, Ilya |
| contents | We present a framework for synthesising formulas in first-order logic (FOL) from examples, which unifies and advances state-of-the-art approaches for inference of transition system invariants. To do so, we study and categorise the existing methodologies, encoding techniques in their formula synthesis via answer set programming (ASP). Based on the derived categorisation, we propose orthogonal slices, a new technique for formula enumeration that partitions the search space into manageable chunks, enabling two approaches for incremental candidate pruning. Using a combination of existing techniques for first-order (FO) invariant synthesis and the orthogonal slices implemented in our framework FORCE, we significantly accelerate a state-of-the-art algorithm for distributed system invariant inference. We also show that our approach facilitates composition of different invariant inference frameworks, allowing for novel optimisations. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_03854 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference Yang, Ziyi Pîrlea, George Sergey, Ilya Programming Languages Logic in Computer Science F.3.1; I.2.2; I.2.3 We present a framework for synthesising formulas in first-order logic (FOL) from examples, which unifies and advances state-of-the-art approaches for inference of transition system invariants. To do so, we study and categorise the existing methodologies, encoding techniques in their formula synthesis via answer set programming (ASP). Based on the derived categorisation, we propose orthogonal slices, a new technique for formula enumeration that partitions the search space into manageable chunks, enabling two approaches for incremental candidate pruning. Using a combination of existing techniques for first-order (FO) invariant synthesis and the orthogonal slices implemented in our framework FORCE, we significantly accelerate a state-of-the-art algorithm for distributed system invariant inference. We also show that our approach facilitates composition of different invariant inference frameworks, allowing for novel optimisations. |
| title | Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference |
| topic | Programming Languages Logic in Computer Science F.3.1; I.2.2; I.2.3 |
| url | https://arxiv.org/abs/2601.03854 |