A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
type: Item
instance of: scholarly article
title: A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
DOI: 10.1007/978-3-030-86205-3_1
author: Martin Bromberger
author: Irina Dragoste
author: Rasha Faqeh
author: Christof Fetzer
author: Markus Krötzsch
author: Christoph Weidenbach
publication date: 2022-03-24T00:00:00Z
full work available at URL: https://arxiv.org/abs/2107.03189
Mathematics Subject Classification ID: 68Txx
zbMATH DE Number: 7497913
describes a project that uses: Isabelle/HOL
describes a project that uses: Spacer
describes a project that uses: Sledgehammer
describes a project that uses: iProver
describes a project that uses: Datalog
describes a project that uses: CVC4
describes a project that uses: VAMPIRE
describes a project that uses: z3
describes a project that uses: SPASS
describes a project that uses: TPTP
MaRDI profile type: Publication
OpenAlex ID: W3202430163
cites work: Refutational theorem proving for hierarchic first-order theories
cites work: Hierarchic superposition revisited
cites work: Horn Clause Solvers for Program Verification
cites work: Sledgehammer: Judgement Day
cites work: Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
cites work: SPASS-SATT. A CDCL(LA) solver
cites work: Universal invariant checking of parametric systems with quantifier-free SMT reasoning
cites work: SCL clause learning from simple models
cites work: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
cites work: Superposition for Bounded Domains
cites work: On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic
cites work: iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
cites work: Complexity results for classes of quantificational formulas
cites work: Applying Linear Quantifier Elimination
cites work: Complexity and related enhancements for automated theorem-proving programs
cites work: Solving SAT and SAT Modulo Theories
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Computing small clause normal forms
cites work: Complete problems in the first-order predicate calculus
cites work: On the verification of security-aware E-services
cites work: Revisiting enumerative instantiation
cites work: Q3150300
cites work: Faster, higher, stronger: E 2.3
cites work: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
cites work: Efficient model construction for Horn logic with VLog (system description)
Recommended article: A linear algebraic approach to datalog evaluation
Recommended article: Datalog LITE
Recommended article: Q2767120
Recommended article: Linearisability on Datalog programs
Recommended article: Solving quantified verification conditions using satisfiability modulo theories
Recommended article: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
Recommended article: Bottom-up evaluation of Datalog programs with arithmetic constraints
Recommended article: A practical approach to satisfiability modulo linear integer arithmetic
Recommended article: A new technique for verifying and correcting logic programs
Recommended article: A verified proof checker for higher-order logic
description: scientific article; zbMATH DE number 7497913