2013 | OriginalPaper | Chapter
Composition-Nominative Logics in Rigorous Development of Software Systems
Authors : Mykola S. Nikitchenko, Valentyn G. Tymofieiev
Published in: Information Systems: Methods, Models, and Applications
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We provide motivation for composition-nominative approach and its main underlying principles. We give a brief introduction to the hierarchy of composition-nominative logics (CNL) and discuss possible applications of these logics in formal approaches for software development. CNL are algebra-based logics of partial predicates and functions. They are constructed in a semantic-syntactic style on the methodological basis, which is common with programming. Main attention in the paper is paid to the first-order CNL. The satisfiability problem for the first-order CNL is addressed. We show the reduction of the problem in hand to the satisfiability problem for classical first-order logic with function symbols. The reduction proposed requires extension of logic language and logic models with an infinite number of unessential variables. The method presented in the paper enables one to use existent satisfiability checking algorithms and tools for solving instances of the CNL satisfiability problem. Thus, many standard techniques developed for classical logics can be applied in CNL-based approaches for program reasoning.