### ?

## Two-sided unification is NP-complete

P. 55-61.

Zakharov V., Новикова Т. А.

It is generally accepted that to unify a pair of substitutions 1 and 2 means to find out
a pair of substitutions 0 and 00 such that the compositions 10 and 200 are the same.
Actually, unification is the problem of solving linear equations of the form 1X = 2Y in
the semigroup of substitutions. But some other linear equations on substitutions may be
also viewed as less common variants of unification problem. In this paper we introduce a
two-sided unification as the process of bringing a given substitution 1 to another given
substitution 2 from both sides by giving a solution to an equation X1Y = 2. Twosided
unification finds some applications in software refactoring as a means for extracting
instances of library subroutines in arbitrary pieces of program code. In this paper we
study the complexity of two-sided unification and show that this problem is NP-complete
by reducing to it the bounded tiling problem.

Language:
English

### In book

Linz : Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, 2014

Zakharov V., Новикова Т. А., Труды Института системного программирования РАН 2014 Т. 26 № 2 С. 245-268

It is generally accepted that to unify a pair of substitutions θ_1 and θ_2 means to find out a pair of substitutions η' and η'' such that the compositions θ_1 η' and θ_2 η'' are the same. Actually, unification is the problem of solving linear equations of the form θ_1 X=θ_2 Y in the semigroup ...

Added: September 30, 2015

Savateev Y., Annals of Pure and Applied Logic 2012 Vol. 163 P. 775-788

In this paper we prove that the derivability problems for product-free Lambek calculus and product-free Lambek calculus allowing empty premises are NP-complete. Also we introduce a new derivability characterization for these calculi. ...

Added: October 20, 2014

Antonopoulos T., Gorogiannis N., Haase C. et al., , in : Lecture Notes in Computer Science. 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. : Berlin : Springer, 2014. Ch. 27. P. 411-425.

We establish foundational results on the computational complexity of deciding entailment in Separation Logic with general inductive predicates whose underlying base language allows for pure formulas, pointers and existentially quantified variables. We show that entailment is in general undecidable, and ExpTime-hard in a fragment recently shown to be decidable by Iosif et al. Moreover, entailment ...

Added: March 24, 2015

Cardilli R., Porcelli S., Rome : Universita Tor Vergata, 2015

Thus book is a collection of articles written on the results of the international scientific seminar "Legal aspects of the BRICS", organized by the University of Rome "Tor Vergata" in May 2013. Lawyers -researchers from Italy, Brazil, Russia, India, China and South Africa Republic took part in the discussion on the harmonization of the legal ...

Added: June 25, 2015

Skopenkov M., Малиновская О. А., Дориченко С. А., Квант 2015 № 2 С. 6-11

In the present popular science paper we determine when a square can be dissected into rectangles similar to a given rectangle. The approach to the question is based on a physical interpretation using electrical networks. Only secondary school background is assumed in the paper. ...

Added: October 16, 2015

Смирнов И. А., Разумов П. В., Болдырихин Н. В. et al., IEEE, 2019

Investigations of cryptographic algorithms for
today are very actually in connection with cybernetic attacks
threat and necessity of information protection at the
enterprises of various levels including the strategic
appointment. The project implementation of John Pollard’s
factorization ρ–method in the programming language C ++ is
presented, which works faster than the standard algorithm by
27%. It can facilitate greatly the deciphering operation ...

Added: May 10, 2023

Zakharov V., Кузюрин Н. Н., Варновский Н. П. et al., Программирование 2015 № 6

Program obfuscation is a semantic-preserving transformation aimed at bringing a program into such a form, which impedes the understanding of its algorithm and data structures or prevents extracting of some valuable information from the text of a program. Since obfuscation could find wide use in computer security, information hiding and cryptography, security requirements to program ...

Added: October 13, 2015

Kasatkina A., Право. Журнал Высшей школы экономики 2012 № 2 С. 144-164

This article devoted the complex analysis governing modern independent codifications of private international law in the countries of South East Asia. As part of this article conducted the detailed analysis of national-legal regulation of laws in the field of private international law in China and Japan. The analysis of the basic institutes of private international ...

Added: November 16, 2012

Kulagin V., Kozina E. O., Grushevenko D., Энергетическая политика 2015 № 1 С. 49-57

The paper analyses the criticality of dependence of Russian oil and gas sector on imported equipment, and presents the specific mechanisms of how effectively and with regard to the state interests ensure the future sustainable development of the sector taking into account technological demands. Particular attention is paid to the creation of the conditions, which ...

Added: May 8, 2015

Zakharyaschev M., BRESOLIN D., KURUCZ A. et al., , in : ACM Transactions on Computational Logic (TOCL). Vol. 18. Issue 3.: NY : ACM, 2017. P. 1-39.

We investigate the satisfiability problem for Horn fragments of the Halpern-Shoham interval temporal logic depending on the type (box or diamond) of the interval modal operators, the type of the underlying linear order (discrete or dense), and the type of semantics for the interval relations (reflexive or irreflexive). For example, we show that satisfiability of ...

Added: September 17, 2017

Shitov Y., SIAM Review 2017 Vol. 59 No. 4 P. 794-800

Using elementary linear algebra, we develop a technique that leads to solutions of two widely known problems on nonnegative matrices. First, we give a short proof of the result by Vavasis stating that the nonnegative rank of a matrix is NP-hard to compute. This proof is essentially contained in the paper by Jiang and Ravikumar, ...

Added: November 9, 2017

Zakharov V., Жайлауова Ш. Р., В кн. : Проблемы теоретической кибернетики: XVIII международная конференция (Пенза, 19-23 июня 2017 г.). : М. : МГУ, МАКС Пресс, 2017. С. 84-87.

Эффективная разрешимость проблемы л-т эквивалентности дает возможность приступить к решению задачи минимизации - построения схемы программ наименьшего размера, л-т эквивалентной заданной схеме. Чтобы отыскать ее решение, заметим, что модель вычислений стандартных схем программ сходна модели вычислений автоматов-преобразователей, работающих над полугруппами. Ранее был предложен метод минимизации автоматов-преобра\-зо\-вателей, работающих над упорядоченными левосократимыми полугруппами. В данной заметке мы ...

Added: October 22, 2017

Zakharov V.A., Kuzurin N. N., Varnovsky N. P. et al., Programming and Computer Software 2015 Vol. 41 No. 6 P. 361-372

Program obfuscation is a semantic-preserving transformation aimed at bringing a program into a form that impedes understanding of its algorithm and data structures or prevents extracting certain valuable information from the text of the program. Since obfuscation may find wide use in computer security, information hiding and cryptography, security requirements to program obfuscators have become ...

Added: October 13, 2015

Kuznetsov S., , in : Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday. Issue 12300.: Cham : Springer, 2020. P. 3-16.

Infinitary action logic is an extension of the multiplicative-additive Lambek calculus with Kleene iteration, axiomatized by an 𝜔-rule. Buszkowski and Palka (2007) show that this logic is \(\Pi^0_1\)-complete. As shown recently by Kuznetsov and Speranski, the extension of infinitary action logic with the exponential modality is much harder: \(\Pi^1_1\)-complete. The raise of complexity is of ...

Added: November 25, 2020

Morgunov A. F., Бизнес-информатика 2014 № 1(27) С. 34-41

The implementation of information system in big company with wide affiliated network in the country, as a rule, is connected with organization and technical difficulties. The process stretches out in time and not always leads to the intended effect.
This article considers the implementation of information system of industrial process automation and workflow of subscriptions for ...

Added: April 9, 2014

Savateev Y., Известия РАН. Серия математическая 2011 Т. 75 № 3 С. 189-222

We use proof-nets to study the algorithmic complexity of the derivability problem for some fragments of the Lambek calculus. We prove the NP-completeness of this problem for the unidirectional fragment and the product-free fragment, and also for versions of these fragments that admit empty antecedents. ...

Added: October 20, 2014

Linz : Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, 2014

Unification is concerned with the problem of identifying terms, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc. The International Workshop on Unification (UNIF) is a yearly forum ...

Added: October 13, 2015

Stepan L. Kuznetsov, Journal of Logic and Computation 2023 Vol. 33 No. 6 P. 1437-1462

We prove undecidability and pinpoint the place in the arithmetical hierarchy for commutative action logic, i.e. the equational theory of commutative residuated Kleene lattices (action lattices), and infinitary commutative action logic, the equational theory of *-continuous commutative action lattices. Namely, we prove that the former is Σ01�10-complete and the latter is Π01�10-complete. Thus, the situation is the ...

Added: March 7, 2023

Medvedeva E., Ryapin I., Urvatsev I. et al., Thermal Engineering (English translation of Teploenergetika) 2016 Vol. 63 No. 9 P. 611-620

This paper analyzes the cost-effectiveness of the use of renewable energy sources (RES) and peat in production of electric and heat energy in rural places of the country by comparing tariffs (prices) of energy versus total expenditures on generation of electric and heat energy when using RES and peat. The appraisal of a cost-effective scale ...

Added: October 9, 2016

Zakharov V., Новикова Т. А., В кн. : Дискретные модели в теории управляющих систем : IX Международная конференция, Москва и Подмосковье, 20-22 мая 2015 г.: Труды. : М. : МАКС Пресс, 2015. С. 173-176.

В статье предложена новая модель последовательных императивных программ, использующих средства работы с динамической памятью (указателями, списками и пр.) ...

Added: October 12, 2015

Kasatkina A., Кобахидзе Д. И., Право и политика 2015 № 8 С. 1112-1128

This article is devoted to the major trends of regulate relations associated with such basic institutions of private international sea law as a maritime lien, rescue ships and other property at sea. These legal institutions not only have special significance in terms of their theoretical study and scientific analysis, but also play an important role ...

Added: August 23, 2015

Rostovtseva N. V., Право. Журнал Высшей школы экономики 2016 № 3 С. 30-49

The paper studies the institute of inheriting per stripes. The main principles specified in the current civil code are in line with the provisions of the Digest of Laws of the Russian Empire. Inheriting per stripes should be differentiated from similar institutes (transmission or substitution). The main difference from transmission consists in the condition that ...

Added: November 27, 2016

Черкесова Л. В., Сафарьян О. А., Смирнов И. А., Молодой исследователь Дона 2018 Т. 3 (12) С. 111-121

The paper presents the project implementation of ρ-factor Pollard factorization in C ++, which works faster than the standard algorithm by 27%, which can significantly facilitate the work in deciphering and cryptanalysis of various ciphers such as RSA ...

Added: May 9, 2023

Lukin A., Pugacheva O., Проблемы Дальнего Востока 2022 № 3 С. 9-27

The paper comprehensively examines Russia's foreign policy towards the Korean Peninsula. Its scientific relevance is defined by the unsettled issues on the Korean Peninsula, including the nuclear one, and the peninsula’s geographical proximity to the Russian Far East, the development of which is a priority task for Russia in the 21st century. The aim of ...

Added: June 27, 2022