Safety- and liveness-properties in propositional temporal logic: characterizations and decidability
Sémantika otázky v problémové situaci
Splitting lattices of logics.
Subalgebras of diagonalizable algebras of theories containing arithmetic [Book]
Sur les algèbres de Heyting symétriques
Taclets: a new paradigm for constructing interactive theorem provers.
Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing proof construction. Such languages are not easy to master and thus contribute to the already long list of skills required by prospective users of interactive theorem provers. Most users, however, only need a convenient formalism that allows to introduce new rules with minimal overhead. On the the other hand, rules...
Tavole semantiche per sistemi astratti di logica estensionale
The Completeness And Compactness Of A Three-Valued First-Order Logic.
The Consistency Of A Variant Of Church's Thesis With An Axiomatic Theory Of An Epistemic Notion.
The elimination of descriptions from A. Bressan’s modal language on which the logical calculus is based
The interpreted type-free modal calculus
The interpreted type-free modal calculus
The interpreted type-free modal calculus . II
The resolution tableau for logics of likelihood
Theorem-proving systems [Book]
Time conditional propositions
Topologies, Continuity and Bisimulations
The notion of a bisimulation relation is of basic importance in many areas of computation theory and logic. Of late, it has come to take a particular significance in work on the formal analysis and verification of hybrid control systems, where system properties are expressible by formulas of the modal μ-calculus or weaker temporal logics. Our purpose here is to give an analysis of the concept of bisimulation, starting with the observation that the zig-zag conditions are suggestive of some...
TTL : a formalism to describe local and global properties of distributed systems
Un principe de résolution en logique modale
Una lógica modal para la geometría esférica de incidencia.
Habitualmente, las geometrías de incidencia están basadas en estructuras bisurtidas formadas por puntos y rectas, y conectadas por una relación entre ambas clases. En lo que sigue, introducimos una estructura monosurtida, que llamamos Marco Esférico de Incidencia, la cual resulta adecuada, para construir una base semántica que permita su consideración en el lenguaje modal. Construiremos así un sistema axiomático para dicho lenguaje, que estaría determinado por la estructura creada, es decir probaremos...