scholarly journals Logic prototyping: approach and use cases

2021 ◽  
Vol 2131 (3) ◽  
pp. 032002
Author(s):  
O A Il’icheva ◽  
V V Ilicheva
Keyword(s):  
Complex Systems ◽  
System Design ◽  
Transport System ◽  
Program Analysis ◽  
Predicate Logic ◽  
Denotational Semantics ◽  
Logical Description ◽  
Logical Errors ◽  
Logic Inference ◽  
Classical Predicate

Abstract In this article, we present an approach to prototyping complex systems and processes using classical predicate logic. The prototype is built by the interpreter based on a logical description of the properties and/or behavior of the designed system. The description contains the definitions of the prototype elements and the constraints that the correct prototype must satisfy. Definitions are used to build a prototype, and constraints are used to analyze it and check the required properties. Definitions are interpreted using direct logic inference, constraints are only checked on the resulting model. A wider class of formulas is used than in well-known logical languages. Computable logical and denotational semantics are defined for them. In the process of building a prototype, logical errors of uncertainty, redefinition of functions, and contradictions are diagnosed. We are given examples of prototype descriptions used for semantic program analysis, space training, transport system design.

UNIFORM INTERPOLATION IN SUBSTRUCTURAL LOGICS

2014 ◽  
Vol 7 (3) ◽  
pp. 455-483 ◽  
Author(s):  
MAJID ALIZADEH ◽  
FARZANEH DERAKHSHAN ◽  
HIROAKIRA ONO
Keyword(s):  
Propositional Logic ◽  
Predicate Logic ◽  
Interpolation Property ◽  
Substructural Logics ◽  
Substructural Logic ◽  
Sequent Calculi ◽  
Structural Rule ◽  
Modal Propositional Logic ◽  
Uniform Interpolation ◽  
Classical Predicate

AbstractUniform interpolation property of a given logic is a stronger form of Craig’s interpolation property where both pre-interpolant and post-interpolant always exist uniformly for any provable implication in the logic. It is known that there exist logics, e.g., modal propositional logic S4, which have Craig’s interpolation property but do not have uniform interpolation property. The situation is even worse for predicate logics, as classical predicate logic does not have uniform interpolation property as pointed out by L. Henkin.In this paper, uniform interpolation property of basic substructural logics is studied by applying the proof-theoretic method introduced by A. Pitts (Pitts, 1992). It is shown that uniform interpolation property holds even for their predicate extensions, as long as they can be formalized by sequent calculi without contraction rules. For instance, uniform interpolation property of full Lambek predicate calculus, i.e., the substructural logic without any structural rule, and of both linear and affine predicate logics without exponentials are proved.

scholarly journals A Formalism for Primitive Logic and Mechanical Proof-Checking

1966 ◽  
Vol 26 ◽  
pp. 195-203 ◽  
Author(s):  
Katuzi Ono
Keyword(s):  
Simple Form ◽  
Predicate Logic ◽  
View Point ◽  
Proof Checking ◽  
Mechanical Proof ◽  
Classical Predicate

The universal character of the primitive logic LO in the sense that popular logics such as the lower classical predicate logic LK, the intuitionistic predicate logic LJ, Johansson’s minimal predicate logic LM, etc. can be faithfully interpreted in LO is very remarkable even from the view point of mechanical proof-checking. Since LO is very simple, deductions in LO could be mechanized in a simple form if a suitable formalism for LO is found out. Main purpose of this paper is to introduce a practical formalism for LO, practical in the sense that it is suitable at least for mechanical proof-checking business.

Toward a Functional Failure Modeling Method of Representing Prognostic Systems During the Early Phases of Design

2015 ◽  
Author(s):  
Caitlin Stack ◽  
Douglas L. Van Bossuyt
Keyword(s):  
Complex System ◽  
Complex Systems ◽  
System Design ◽  
Power Plants ◽  
Pressurized Water ◽  
Functional Failure ◽  
Early Stages ◽  
Failure Modeling ◽  
Complex System Design ◽  
Early Phases

Current methods of functional failure risk analysis do not facilitate explicit modeling of systems equipped with Prognostics and Health Management (PHM) hardware. As PHM systems continue to grow in application and popularity within major complex systems industries (e.g. aerospace, automotive, civilian nuclear power plants), implementation of PHM modeling within the functional failure modeling methodologies will become useful for the early phases of complex system design and for analysis of existing complex systems. Functional failure modeling methods have been developed in recent years to assess risk in the early phases of complex system design. However, the methods of functional modeling have yet to include an explicit method for analyzing the effects of PHM systems on system failure probabilities. It is common practice within the systems health monitoring industry to design the PHM subsystems during the later stages of system design — typically after most major system architecture decisions have been made. This practice lends itself to the omission of considering PHM effects on the system during the early stages of design. This paper proposes a new method for analyzing PHM subsystems’ contribution to risk reduction in the early stages of complex system design. The Prognostic Systems Variable Configuration Comparison (PSVCC) eight-step method developed here expands upon existing methods of functional failure modeling by explicitly representing PHM subsystems. A generic pressurized water nuclear reactor primary coolant loop system is presented as a case study to illustrate the proposed method. The success of the proposed method promises more accurate modeling of complex systems equipped with PHM subsystems in the early phases of design.

A proof-theoretic study of the correspondence of classical logic and modal logic

2003 ◽  
Vol 68 (4) ◽  
pp. 1403-1414 ◽  
Author(s):  
H. Kushida ◽  
M. Okada
Keyword(s):  
Modal Logic ◽  
Classical Logic ◽  
Predicate Logic ◽  
Transformation Method ◽  
Modal Operator ◽  
Theoretic Method ◽  
Barcan Formula ◽  
Theoretic Proof ◽  
Classical Predicate

AbstractIt is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof.

Sign in / Sign up

Export Citation Format

Share Document