scholarly journals The ∃*∀* Part of the Theory of Ground Term Algebra Modulo an AC Symbol is Undecidable

2002 ◽  
Vol 178 (2) ◽  
pp. 412-421
Author(s):  
Jerzy Marcinkowski
Keyword(s):  
Ground Term ◽  
Term Algebra

scholarly journals Nominal Equational Problems

2021 ◽  
pp. 22-41
Author(s):  
Mauricio Ayala-Rincón ◽  
Maribel Fernández ◽  
Daniele Nantes-Sobrinho ◽  
Deivid Vale
Keyword(s):  
General Definition ◽  
Ground Term ◽  
First Order ◽  
Rule Application ◽  
Definition Of ◽  
Term Algebra

AbstractWe define nominal equational problems of the form $$\exists \overline{W} \forall \overline{Y} : P$$ ∃ W ¯ ∀ Y ¯ : P , where $$P$$ P consists of conjunctions and disjunctions of equations $$s\approx _\alpha t$$ s ≈ α t , freshness constraints $$a\#t$$ a # t and their negations: $$s \not \approx _\alpha t$$ s ≉ α t and "Equation missing", where $$a$$ a is an atom and $$s, t$$ s , t nominal terms. We give a general definition of solution and a set of simplification rules to compute solutions in the nominal ground term algebra. For the latter, we define notions of solved form from which solutions can be easily extracted and show that the simplification rules are sound, preserving, and complete. With a particular strategy for rule application, the simplification process terminates and thus specifies an algorithm to solve nominal equational problems. These results generalise previous results obtained by Comon and Lescanne for first-order languages to languages with binding operators. In particular, we show that the problem of deciding the validity of a first-order equational formula in a language with binding operators (i.e., validity modulo $$\alpha $$ α -equality) is decidable.

Foundation for Model Integration: Semantic Backplane

2012 ◽  
Author(s):  
Gabor Simko ◽  
Tihamer Levendovszky ◽  
Sandeep Neema ◽  
Ethan Jackson ◽  
Ted Bapty ◽  
...  
Keyword(s):  
Design Flow ◽  
Model Transformations ◽  
Model Integration ◽  
Mathematical Framework ◽  
Modeling Languages ◽  
Tool Chain ◽  
Model Based ◽  
Essential Properties ◽  
The Individual ◽  
Term Algebra

One of the primary goals of the Adaptive Vehicle Make (AVM) program of DARPA is the construction of a model-based design flow and tool chain, META, that will provide significant productivity increase in the development of complex cyber-physical systems. In model-based design, modeling languages and their underlying semantics play fundamental role in achieving compositionality. A significant challenge in the META design flow is the heterogeneity of the design space. This challenge is compounded by the need for rapidly evolving the design flow and the suite of modeling languages supporting it. Heterogeneity of models and modeling languages is addressed by the development of a model integration language – CyPhy – supporting constructs needed for modeling the interactions among different modeling domains. CyPhy targets simplicity: only those abstractions are imported from the individual modeling domains to CyPhy that are required for expressing relationships across sub-domains. This “semantic interface” between CyPhy and the modeling domains is formally defined, evolved as needed and verified for essential properties (such as well-formedness and invariance). Due to the need for rapid evolvability, defining semantics for CyPhy is not a “one-shot” activity; updates, revisions and extensions are ongoing and their correctness has significant implications on the overall consistency of the META tool chain. The focus of this paper is the methods and tools used for this purpose: the META Semantic Backplane. The Semantic Backplane is based on a mathematical framework provided by term algebra and logics, incorporates a tool suite for specifying, validating and using formal structural and behavioral semantics of modeling languages, and includes a library of metamodels and specifications of model transformations.

Simple and Minimal Ground Term Equation Systems

1998 ◽  
Vol 36 (4) ◽  
pp. 367-413 ◽  
Author(s):  
Sándor Vágvölgyi
Keyword(s):  
Ground Term

The Origin of the Term “Algebra”

1926 ◽  
Vol 33 (9) ◽  
pp. 437-440
Author(s):  
Solomon Gandz
Keyword(s):  
Term Algebra

Elektronische und Resonanz-Raman-Spektren der Chloro-Bromo-Ruthenate(IV), [RuClnBr6-n]2-, n = 0 ... 6

1987 ◽  
Vol 42 (6) ◽  
pp. 597-602
Author(s):  
H. N. v. Allwörden ◽  
W. Preetz
Keyword(s):  
Fine Structure ◽  
Spin Orbit Coupling ◽  
Spin Orbit ◽  
Tetraalkylammonium Salts ◽  
Ground Term ◽  
Point Groups ◽  
Resonance Raman Spectra ◽  
And Shifts ◽  
Electronic Resonance ◽  
Polarisation Measurements

The vibrational and electronic resonance Raman spectra of the solid tetraalkylammonium salts of [RuClnBr6-n]2-, n = 0 . . . 6, are measured at 80 K. The observed electronic Raman bands in the regions of 640-740 cm-1 and 1560-1790 cm-1 are assigned to the intraconfigurational transitions Γ1 → Γ4 and Γ1 → Γ3, Γ5 within the 3T1g(Oh) ground term. The observed splittings and shifts, due to spin orbit coupling and lowered symmetry, are interpreted qualitatively according to the point groups D4h, C4V, C3V and C2V. The O-O-transitions are deduced from vibrational fine structure. The electronic Raman bands of [RuCl6]2- and [RuBr6]2- are assigned in detail by polarisation measurements.

Sign in / Sign up

Export Citation Format

Share Document