A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3202430163
@@ Property / OpenAlex ID: W3202430163 / rank @@
+Normal rank
@@ Property / cites work @@
+Refutational theorem proving for hierarchic first-order theories
+Normal rank
@@ Property / cites work @@
+Hierarchic superposition revisited
@@ Property / cites work: Hierarchic superposition revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Horn Clause Solvers for Program Verification
@@ Property / cites work: Horn Clause Solvers for Program Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Sledgehammer: Judgement Day
@@ Property / cites work: Sledgehammer: Judgement Day / rank @@
+Normal rank
@@ Property / cites work @@
+A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
+Normal rank
@@ Property / cites work @@
+Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
+Normal rank
@@ Property / cites work @@
+SPASS-SATT. A CDCL(LA) solver
@@ Property / cites work: SPASS-SATT. A CDCL(LA) solver / rank @@
+Normal rank
@@ Property / cites work @@
+Universal invariant checking of parametric systems with quantifier-free SMT reasoning
+Normal rank
@@ Property / cites work @@
+SCL clause learning from simple models
@@ Property / cites work: SCL clause learning from simple models / rank @@
+Normal rank
@@ Property / cites work @@
+Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
+Normal rank
@@ Property / cites work @@
+Superposition for Bounded Domains
@@ Property / cites work: Superposition for Bounded Domains / rank @@
+Normal rank
@@ Property / cites work @@
+On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic
+Normal rank
@@ Property / cites work @@
+iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
+Normal rank
@@ Property / cites work @@
+Complexity results for classes of quantificational formulas
+Normal rank
@@ Property / cites work @@
+Applying Linear Quantifier Elimination
@@ Property / cites work: Applying Linear Quantifier Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+Complexity and related enhancements for automated theorem-proving programs
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q2751358
@@ Property / cites work: Q2751358 / rank @@
+Normal rank
@@ Property / cites work @@
+Complete problems in the first-order predicate calculus
+Normal rank
@@ Property / cites work @@
+On the verification of security-aware E-services
@@ Property / cites work: On the verification of security-aware E-services / rank @@
+Normal rank
@@ Property / cites work @@
+Revisiting enumerative instantiation
@@ Property / cites work: Revisiting enumerative instantiation / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150300
@@ Property / cites work: Q3150300 / rank @@
+Normal rank
@@ Property / cites work @@
+Faster, higher, stronger: E 2.3
@@ Property / cites work: Faster, higher, stronger: E 2.3 / rank @@
+Normal rank
@@ Property / cites work @@
+The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
+Normal rank
@@ Property / cites work @@
+Efficient model construction for Horn logic with VLog (system description)
+Normal rank