Cover Image

Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Yang, Ziyi, Pîrlea, George, Sergey, Ilya
Format:	Preprint
Published:	2026
Subjects:	Programming Languages Logic in Computer Science F.3.1; I.2.2; I.2.3
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Proving Cutoff Bounds for Safety Properties in First-Order Logic
by: Lotan, Raz, et al.
Published: (2024)

Implicit Rankings for Verifying Liveness Properties in First-Order Logic
by: Lotan, Raz, et al.
Published: (2024)

Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
by: Lotan, Raz, et al.
Published: (2026)

From Scientific Texts to Verifiable Code: Automating the Process with Transformers
by: Wang, Changjie, et al.
Published: (2025)

The Stable Model Semantics for Higher-Order Logic Programming
by: Bogaerts, Bart, et al.
Published: (2024)

Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs
by: de Rezende, Susanna F., et al.
Published: (2019)

Non-Ground Congruence Closure
by: Leidinger, Hendrik, et al.
Published: (2024)

ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings
by: Jana, Prithwish, et al.
Published: (2025)

Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned
by: Villadsen, Jørgen
Published: (2025)

Test Case Features as Hyper-heuristics for Inductive Programming
by: McDaid, Edward, et al.
Published: (2024)

A Sequent Calculus for General Inductive Definitions
by: Eede, Robbe Van den, et al.
Published: (2026)

A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
by: Klaus, Natalia, et al.
Published: (2026)

Unravelling Abstract Cyclic Proofs into Proofs by Induction
by: Grotenhuis, Lide, et al.
Published: (2026)

Teaching Higher-Order Logic Using Isabelle
by: Lund, Simon Tobias, et al.
Published: (2024)

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation
by: Bertrand, Meven Lennon, et al.
Published: (2026)

Instruction and Solution Probabilities as Heuristics for Inductive Programming
by: McDaid, Edward, et al.
Published: (2025)

FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines
by: Zhang, Xindi, et al.
Published: (2025)

SPARQL in N3: SPARQL CONSTRUCT as a rule language for the Semantic Web (Extended Version)
by: Arndt, Dörthe, et al.
Published: (2025)

Proof-Carrying Neuro-Symbolic Code
by: Komendantskaya, Ekaterina
Published: (2025)

A Proof System with Causal Labels (Part II): checking Counterfactual Fairness
by: Ceragioli, Leonardo, et al.
Published: (2025)

A Proof System with Causal Labels (Part I): checking Individual Fairness and Intersectionality
by: Ceragioli, Leonardo, et al.
Published: (2025)

A Coq-based Axiomatization of Tarski's Mereogeometry
by: Barlatier, Patrick, et al.
Published: (2025)

Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl)
by: van Brügge, Jan
Published: (2024)

Term Orders for Optimistic Lambda-Superposition
by: Bentkamp, Alexander, et al.
Published: (2025)

Implementing the First-Order Logic of Here and There
by: Otten, Jens, et al.
Published: (2026)

AgenticTyper: Automated Typing of Legacy Software Projects Using Agentic AI
by: Pohle, Clemens
Published: (2026)

Definite Descriptions and Hybrid Tense Logic
by: Indrzejczak, Andrzej, et al.
Published: (2024)

Executable First-Order Queries in the Logic of Information Flows
by: Aamer, Heba, et al.
Published: (2022)

Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
by: Lin, Hongyu, et al.
Published: (2026)

SPARTA: Scalable and Principled Benchmark of Tree-Structured Multi-hop QA over Text and Tables
by: Park, Sungho, et al.
Published: (2026)

Summa Summarum: Moessner's Theorem without Dynamic Programming
by: Danvy, Olivier
Published: (2024)

Data Verification is the Future of Quantum Computing Copilots
by: Song, Junhao, et al.
Published: (2026)

Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries
by: McCann, Alan L.
Published: (2026)

Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
by: McCann, Alan L.
Published: (2026)

Algorithmic Trading Strategy Development and Optimisation
by: Yuan, Owen Nyo Wei, et al.
Published: (2026)

Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates
by: Echenim, Mnacho, et al.
Published: (2023)

Automating the Analysis of Parsing Algorithms (and other Dynamic Programs)
by: Vieira, Tim, et al.
Published: (2025)

Hybrid Game Control Envelope Synthesis
by: Kabra, Aditi, et al.
Published: (2025)

The Relational Machine Calculus
by: Barrett, Chris, et al.
Published: (2024)

Large Language Models Are Not Strong Abstract Reasoners
by: Gendron, Gaël, et al.
Published: (2023)