Axiomatic Constraint Systems for Proof Search Modulo Theories

DOI10.1007/978-3-319-24246-0_14zbMath1471.68317arXiv1412.6790OpenAlexW312152708MaRDI QIDQ2964465

Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, Damien Rouhling, Jean-Marc 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

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)

Uses Software

• Psyche

Cites Work

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

This page was built for publication: Axiomatic Constraint Systems for Proof Search Modulo Theories