Axiomatic constraint systems for proof search modulo theories

DOI10.1007/978-3-319-24246-0_14zbMATH Open1471.68317arXiv1412.6790OpenAlexW312152708MaRDI QIDQ2964465FDOQ2964465

Authors: Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, J. M. Notin 

Publication date: 27 February 2017

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Abstract: Goal-directed proof search in first-order logic uses meta-variables to delay the choice of witnesses; substitutions for such variables are produced when closing proof-tree branches, using first-order unification or a theory-specific background reasoner. This paper investigates a generalisation of such mechanisms whereby theory-specific constraints are produced instead of substitutions. In order to design modular proof-search procedures over such mechanisms, we provide a sequent calculus with meta-variables, which manipulates such constraints abstractly. Proving soundness and completeness of the calculus leads to an axiomatisation that identifies the conditions under which abstract constraints can be generated and propagated in the same way unifiers usually are. We then extract from our abstract framework a component interface and a specification for concrete implementations of background reasoners.

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

Recommendations

• Disjunction and modular goal-directed proof search
• Experimenting with deduction modulo
• Theorem proving modulo
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Investigations into proof-search in a system of first-order dependent function types

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture
• Solving SAT and SAT Modulo Theories
• Automated deduction by theory resolution
• Adding decision procedures to SMT solvers using axioms with triggers
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• Model Evolution with Equality Modulo Built-in Theories
• Title not available (Why is that?)
• Equality and other theories
• (LIA) - Model Evolution with Linear Integer Arithmetic Constraints

Cited In (1)

• Title not available (Why is that?)

Uses Software

• Psyche

This page was built for publication: Axiomatic constraint systems for proof search modulo theories

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