China
Africa
Explore chapters and articles related to this topic
Automatic Software Verification Based on Reverse Engineering and Deduction: A Brief Description of the Alice System
Published in Don Potter, Manton Matthews, Moonis Ali, Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, 2020
Vicent R. Palasí, Francisco Toledo
If we wish to study the correctness of this function, we must have to write a specification of it. The result (using initial semantics) can be seen at Figure 2b5. Following the general idea explained in Section 2, we transform function “*” into the specification SP2 showed in Figure 2c6 (via the Reverse Engineering Process). In our approach, we can say that function “*” is correct w.r.t. specification SP1 if specifications SP1 and SP2 (which is the algebraic semantics of function “*”) are “equivalent”.
Two proofs of the algebraic completeness theorem for multilattice logic
Published in Journal of Applied Non-Classical Logics, 2019
Oleg Grigoriev, Yaroslav Petrukhin
Shramko presented two proof systems for : a binary consequence system with multiple consequence relations2 and a sequent calculus. He introduced an algebraic semantics for which is based on the concept of multilattice. Moreover, Shramko formulated two algebraic completeness theorems, but without proofs. He has just mentioned that algebraic completeness of the binary consequence system for (Shramko, 2016, Theorem 4.8) can be proved by Odintsov and Wansing's method (Odintsov & Wansing, 2015, Theorem 3.7) and algebraic completeness of the sequent calculus for (Shramko, 2016, Theorem 5.5) can be proved by Arieli and Avron's method (Arieli & Avron, 1996).
Polynomial semantics for modal logics
Published in Journal of Applied Non-Classical Logics, 2019
Juan C. Agudelo-Agudelo, Santiago Echeverri-Valencia
Taking into account the results in Agudelo-Agudelo et al. (2016) and the results here, the class of propositional logics characterisable by polynomial semantics is really huge, including every finite-valued logic, every finite extension of the modal logic K and several paraconsistent logics. This is perhaps a sign that polynomial semantics is a powerful alternative to the usual algebraic semantics. Thus, we hope that the results here encourage other people to work in this new algebraic semantics, searching for polynomial characterisations of other kind of logics, analysing this kind of semantics and their relations with the usual algebraic semantics in an abstract way, establishing more connections between algebraic properties of polynomials and logic questions, or working in any other direction.
Monoidal logics: completeness and classical systems
Published in Journal of Applied Non-Classical Logics, 2019
First, the objective is to establish the completeness of monoidal logics with respect to Goré's associative display calculus. To accomplish this, we begin in Section 2 by presenting the proof theory of monoidal and display logics. Given that these two frameworks have already been discussed at length, we only provide what is necessary for the topic of the current paper and refer the reader to the appropriate references for further discussion. The completeness result is provided in Section 3, where we show that a proof is derivable within specific monoidal deductive systems if and only if the sequent is derivable within their corresponding display counterpart (with and appropriate translations). As a result, monoidal logics are sound and complete with regards to the algebraic semantics of display and substructural logics.