Axiomatic constraint systems for proof search modulo theories

DOI10.1007/978-3-319-24246-0_14MaRDI QIDQ2964465zbMATH OpenOpenAlexFDO

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)

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

Mathematics Subject Classification ID

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

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.

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

Cites work

• (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• Adding decision procedures to SMT solvers using axioms with triggers
• Automated deduction by theory resolution
• Equality and other theories
• scientific article; zbMATH DE number 1552529 (Why is no real title available?)
• Model Evolution with Equality Modulo Built-in Theories
• Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)

Cited in

(3)

• Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture
• scientific article; zbMATH DE number 4191139 (Why is no real title available?)
• Disjunction and modular goal-directed proof search

Describes a project that uses

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)