scholarly journals Basic Logic, SMT solvers and finitely generated varieties of GBL-algebras

10.29007/nptc ◽  
2018 ◽  
Author(s):  
Peter Jipsen
Keyword(s):  
Decision Procedure ◽  
Satisfiability Modulo Theories ◽  
Basic Logic ◽  
Finitely Generated ◽  
Logic Formula ◽  
Smt Solvers ◽  
Effective Decision ◽  
Closure Algebras

We show how to implement an effective decision procedure to check if a propositional Basic Logic formula is a tautology. For a formula with $n$ variables, the procedure consists of a translation, depending on $n$, from Basic Logic to the language of Satisfiability Modulo Theories SMT-LIB2 using the theory of quantifier free linear real arithmetic. Many efficient SMT-solvers exist to decide formulas in the SMT-LIB2 language. We also study finitely generated varieties of Basic Logic (BL-)algebras and give a description of the lattice of these varieties. Extensions to finitely generated varieties of Generalized BL-algebras are discussed, and a simple connection between finite GBL-algebras and finite closure algebras is noted.

scholarly journals A Decision Procedure for (Co)datatypes in SMT Solvers

2016 ◽  
Vol 58 (3) ◽  
pp. 341-362 ◽  
Author(s):  
Andrew Reynolds ◽  
Jasmin Christian Blanchette
Keyword(s):  
Decision Procedure ◽  
Smt Solvers

Decompositions of finitely generated modules over C(X): sheaf semantics and a decision procedure

1988 ◽  
Vol 103 (2) ◽  
pp. 257-268
Author(s):  
Andre Scedrov ◽  
Philip Scowcroft
Keyword(s):  
Decision Procedure ◽  
Operator Algebras ◽  
Finitely Generated ◽  
Complex Functions ◽  
Continuous Complex ◽  
Finitely Generated Modules

In the theory of operator algebras the rings of finite matrices over such algebras play a very important role (see [10]). For commutative operator algebras, the Gelfand-Naimark representation allows one to concentrate on matrices over rings of continuous complex functions on compact Hausdorif spaces.

scholarly journals JavaSMT 3: Interacting with SMT Solvers in Java

2021 ◽  
pp. 195-208
Author(s):  
Daniel Baier ◽  
Dirk Beyer ◽  
Karlheinz Friedberger
Keyword(s):  
Programming Languages ◽  
Satisfiability Modulo Theories ◽  
Performance Characteristics ◽  
Enabling Technology ◽  
Smt Solvers ◽  
Computer Aided ◽  
And Performance ◽  
Lock In Effect ◽  
Lock In ◽  
Update Process

AbstractSatisfiability Modulo Theories (SMT) is an enabling technology with many applications, especially in computer-aided verification. Due to advances in research and strong demand for solvers, there are many SMT solvers available. Since different implementations have different strengths, it is often desirable to be able to substitute one solver by another. Unfortunately, the solvers have vastly different APIs and it is not easy to switch to a different solver (lock-in effect). To tackle this problem, we developed JavaSMT, which is a solver-independent framework that unifies the API for using a set of SMT solvers. This paper describes version 3 of JavaSMT, which now supports eight SMT solvers and offers a simpler build and update process. Our feature comparisons and experiments show that different SMT solvers significantly differ in terms of feature support and performance characteristics. A unifying Java API for SMT solvers is important to make the SMT technology accessible for software developers. Similar APIs exist for other programming languages.

Functional verification of cyber-physical systems containing machine-learnt components

2021 ◽  
Vol 0 (0) ◽  
Author(s):  
Farzaneh Moradkhani ◽  
Martin Fränzle
Keyword(s):  
Neural Network ◽  
Machine Learning ◽  
Neural Networks ◽  
Cyber Physical Systems ◽  
Satisfiability Modulo Theories ◽  
Activation Functions ◽  
Physical Systems ◽  
Smt Solvers ◽  
Non Linear ◽  
Artificial Neural

Abstract Functional architectures of cyber-physical systems increasingly comprise components that are generated by training and machine learning rather than by more traditional engineering approaches, as necessary in safety-critical application domains, poses various unsolved challenges. Commonly used computational structures underlying machine learning, like deep neural networks, still lack scalable automatic verification support. Due to size, non-linearity, and non-convexity, neural network verification is a challenge to state-of-art Mixed Integer linear programming (MILP) solvers and satisfiability modulo theories (SMT) solvers [2], [3]. In this research, we focus on artificial neural network with activation functions beyond the Rectified Linear Unit (ReLU). We are thus leaving the area of piecewise linear function supported by the majority of SMT solvers and specialized solvers for Artificial Neural Networks (ANNs), the successful like Reluplex solver [1]. A major part of this research is using the SMT solver iSAT [4] which aims at solving complex Boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and therefore is suitable to verify the safety properties of a specific kind of neural network known as Multi-Layer Perceptron (MLP) which contain non-linear activation functions.

scholarly journals Modular strategic SMT solving with SMT-RAT

2018 ◽  
Vol 10 (1) ◽  
pp. 5-25 ◽  
Author(s):  
Gereon Kremer ◽  
Erika Ábrahám
Keyword(s):  
Satisfiability Modulo Theories ◽  
Integer Arithmetic ◽  
Smt Solving ◽  
Smt Solvers

Abstract In this paper we present the latest developments in SMT-RAT, a tool for the automated check of quantifier-free real and integer arithmetic formulas for satisfiability. As a distinguishing feature, SMT-RAT provides a set of solving modules and supports their strategic combination. We describe our CArL library for arithmetic computations, the available modules implemented on top of CArL, and how modules can be combined to satisfiability-modulo-theories (SMT) solvers. Besides the traditional SMT approach, some new modules support also the recently proposed and highly promising model-constructing satisfiability calculus approach.

ON THE STAR HEIGHT OF RATIONAL LANGUAGES

1994 ◽  
Vol 04 (03) ◽  
pp. 427-441 ◽  
Author(s):  
ROSA MONTALBANO ◽  
ANTONIO RESTIVO
Keyword(s):  
Decision Procedure ◽  
Point Of View ◽  
Finitely Generated ◽  
Algebraic Point ◽  
Rational Language

Two problems concerning the star height of a rational language are investigated: the star height one problem and the relationships between the unambiguity of an expression and its star height. For this purpose we consider the class of factorial, transitive and rational (FTR) languages. From the algebraic point of view a FTR language is the set of factors of a rational submonoid M. Two subclasses of FTR languages are introduced: renewal languages, corresponding to the case of M finitely generated, and unambiguous renewal languages, corresponding to the case of M finitely generated and free. We prove that a FTR language has star height one if and only if it is renewal. This gives a simple decision procedure for the star height one problem for this class of languages. As concerns the relationships with the ambiguity, we introduce the notion of unambiguous star height of a rational language and prove that it can be strictly greater than the star height. This is a consequence of the following results: i) a FTR language of unambiguous star height one is unambiguous renewal; ii) there exist renewal languages which are not unambiguous renewal. This last result is obtained by using arguments involving the entropy of a language.

ON BEGINS, MEETS AND BEFORE

2012 ◽  
Vol 23 (03) ◽  
pp. 559-583 ◽  
Author(s):  
DAVIDE BRESOLIN ◽  
PIETRO SALA ◽  
GUIDO SCIAVICCO
Keyword(s):  
Temporal Logic ◽  
Decision Procedure ◽  
Linear Models ◽  
Complete Classification ◽  
Temporal Logics ◽  
Logic Formula ◽  
Current Interval ◽  
Finite Domains ◽  
Interval Temporal Logics

Interval temporal logics (ITLs) are logics for reasoning about temporal statements expressed over intervals, i.e., periods of time. The most famous temporal logic for intervals studied so far is probably Halpern and Shoham's HS, which is the logic of the thirteen Allen's interval relations. Unfortunately, HS and most of its fragments are undecidable. This discouraged the research in this area until recently, when a number non-trivial decidable ITLs have been discovered. This paper is a contribution towards the complete classification of all different fragments of HS. We consider here different combinations of the interval relations begins (B), meets (A), later (L) and their inverses [Formula: see text], [Formula: see text] and [Formula: see text]. We know from previous work that the combination [Formula: see text] is decidable only when finite domains are considered (and undecidable elsewhere), and that [Formula: see text] is decidable over the natural numbers. In the present paper we show that, over strongly discrete linear models (e.g. finite orders, the naturals, the integers), decidability of [Formula: see text] can be further extended to capture the language [Formula: see text], which lies strictly in between [Formula: see text] and [Formula: see text]. The logic [Formula: see text] turns out to be maximal w.r.t decidability over the considered classes, and its satisfiability problem is EXPSPACE-complete. In this paper we also provide an optimal non-deterministic decision procedure, and we show that the language is powerful enough to polynomially encode metric constraints on the length of the current interval.

scholarly journals Personnel Scheduling as Satisfiability Modulo Theories

2017 ◽  
Author(s):  
Christoph Erkinger ◽  
Nysret Musliu
Keyword(s):  
Real Life ◽  
Satisfiability Modulo Theories ◽  
Compact Representation ◽  
Workforce Scheduling ◽  
Exact Methods ◽  
First Order ◽  
Smt Solvers ◽  
Benchmark Instances ◽  
Modeling Techniques ◽  
New Formulation

Rotating workforce scheduling (RWS) is an important real-life personnel rostering problem that appears in a large number of different business areas. In this paper, we propose a new exact approach to RWS that exploits the recent advances on Satisfiability Modulo Theories (SMT). While solving can be automated by using a number of so-called SMT-solvers, the most challenging task is to find an efficient formulation of the problem in first-order logic. We propose two new modeling techniques for RWS that encode the problem using formulas over different background theories. The first encoding provides an elegant approach based on linear integer arithmetic. Furthermore, we developed a new formulation based on bitvectors in order to achieve a more compact representation of the constraints and a reduced number of variables. These two modeling approaches were experimentally evaluated on benchmark instances from literature using different state-of-the-art SMT-solvers. Compared to other exact methods, the results of this approach showed an important improvement in the number of found solutions.

scholarly journals Towards Strong Higher-Order Automation for Fast Interactive Verification

10.29007/3ngx ◽  
2018 ◽  
Author(s):  
Jasmin Christian Blanchette ◽  
Pascal Fontaine ◽  
Stephan Schulz ◽  
Uwe Waldmann
Keyword(s):  
Research Council ◽  
Higher Order ◽  
Point Of View ◽  
Satisfiability Modulo Theories ◽  
Proof Assistants ◽  
First Order ◽  
The Core ◽  
Proof Rules ◽  
Level Of Automation ◽  
Smt Solvers

We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. From this point of view, it seems desirable to enrich superposition and SMT (satisfiability modulo theories) with higher-order reasoning in a careful manner, to preserve their good properties. Representative benchmarks from the interactive community can guide the design of proof rules and strategies. With higher-order superposition and higher-order SMT in place, highly automatic provers could be built on modern superposition provers and SMT solvers, following a stratified architecture reminiscent of that of modern SMT solvers. We hope that these provers will bring a new level of automation to the users of proof assistants. These challenges and work plan are at the core of the Matryoshka project, funded for five years by the European Research Council. We encourage researchers motivated by the same goals to get in touch with us, subscribe to our mailing list, and join forces.

scholarly journals Conflicts, Models and Heuristics for Quantifier Instantiation in SMT

10.29007/jmd3 ◽  
2018 ◽  
Author(s):  
Andrew Reynolds
Keyword(s):  
Formal Methods ◽  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Software Verification ◽  
Satisfiability Modulo Theories ◽  
Smt Solvers ◽  
Recent Advances ◽  
Common Technique ◽  
Quantifier Instantiation ◽  
Future Work

Satisfiability Modulo Theories (SMT) solvers have emerged as prominent tools in formal methods applications. While originally targeted towards quantifier-free inputs, SMT solvers are now often used for handling quantified formulas in automated theorem proving and software verification applications. The most common technique for handling quantified formulas in modern SMT solvers in quantifier instantiation. This paper gives an overview of recent advances in quantifier instantiation in SMT. In addition to the well-known technique known as E-matching, we discuss the use of conflicts and models for accelerating the search for (un)satisfiably. We further mention new instantiation-based techniques that are specialized to background theories such as linear real and integer arithmetic, and future work in this direction.

Sign in / Sign up

Export Citation Format

Share Document