ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
Filter
  • Computer Programming and Software  (8)
  • (α-Aminoalkyl)phosphonic acids  (1)
  • 2000-2004  (9)
  • 1
    Electronic Resource
    Electronic Resource
    An Efficient One-Pot Synthesis of New Polyfunctional Phosphorus Acid Amphiphiles (2000)
    Weinheim : Wiley-Blackwell
    Liebigs Annalen 2000 (2000), S. 281-289 
    Details
    ISSN: 1434-193X
    Keywords: Phosphorus acid amphiphiles ; (α-Aminoalkyl)phosphonic acids ; Carboxyalkyl (α-aminoalkyl)phosphonic acid monoesters ; Spiro compounds ; Pudovik reaction ; Chemistry ; General Chemistry
    Source: Wiley InterScience Backfile Collection 1832-2000
    Topics: Chemistry and Pharmacology
    Notes: ---The addition reaction between the P-H bond of tetraoxyspirophosphoranes 1-2 and long-chain imines 3a-h (decyl, dodecyl, tetradecyl, hexadecyl, octadecyl, and oleyl imines) occurs instantaneously at room temperature. It is diastereoselective, and quantitatively leads to the corresponding (α-aminoalkyl)spirophosphoranes 4a-h and 5e. The influence of the pentacoordinated phosphorus atom on the stereoselectivity of the Pudovik reaction might be attributed to the involvement of the rigid spirophosphoranide (PV) intermediate in the addition reaction. Selective and one-pot hydrolysis of these P-C bond spirophosphoranes readily proceeds either at room temperature in the presence of moist solvents to give the corresponding carboxyalkyl (α-aminoalkyl)phosphonic acid monoesters 6a-h and 7e, or the reaction may be carried out in the presence of 20% aqueous hydrochloric acid under reflux, to afford the free (α-aminoalkyl)phosphonic acid amphiphiles 8a-h in high yields. In contrast to their sodium salts, these single- and double-chained free and monoester phosphonic acid amphiphiles exist as zwitterions and are not soluble in water.
    Additional Material: 2 Tab.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
  • 2
    facet.materialart.
    Unknown
    Developing User Strategies in PVS: A Tutorial (2003)
    In:  CASI
    Details
    Publication Date: 2018-06-11
    Description: This tutorial provides an overview of the PVS strategy language, and explains how to define new PVS strategies and load them into PVS, and how to create a strategy package. It then discusses several useful techniques that can be used in developing user strategies, and provides examples that illustrate many of these techniques.
    Keywords: Computer Programming and Software
    Type: Design and Application of Strategies/Tactics in Higher Order Logics; 16-42; NASA/CP-2003-212448
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 3
    facet.materialart.
    Unknown
    Explicit Substitutions and All That (2000)
    In:  CASI
    Details
    Publication Date: 2019-08-17
    Description: Explicit substitution calculi are extensions of the lambda-calculus where the substitution mechanism is internalized into the theory. This feature makes them suitable for implementation and theoretical study of logic-based tools such as strongly typed programming languages and proof assistant systems. In this paper we explore new developments on two of the most successful styles of explicit substitution calculi: the lambda sigma- and lambda S(e)-calculi.
    Keywords: Computer Programming and Software
    Type: AD-A385383 , ICASE-2000-45 , NASA-CR-2000-210621
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 4
    facet.materialart.
    Unknown
    Real Automation in the Field (2001)
    In:  CASI
    Details
    Publication Date: 2019-07-10
    Description: We provide a package of strategies for automation of non-linear arithmetic in PVS. In particular, we describe a simplication procedure for the field of real numbers and a strategy for cancellation of common terms.
    Keywords: Computer Programming and Software
    Type: NASA/CR-2001-211271 , NAS 1.26:211271 , ICASE-39
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 5
    facet.materialart.
    Unknown
    On the Formal Verification of Conflict Detection Algorithms (2001)
    In:  CASI
    Details
    Publication Date: 2019-07-10
    Description: Safety assessment of new air traffic management systems is a main issue for civil aviation authorities. Standard techniques such as testing and simulation have serious limitations in new systems that are significantly more autonomous than the older ones. In this paper, we present an innovative approach, based on formal verification, for establishing the correctness of conflict detection systems. Fundamental to our approach is the concept of trajectory, which is a continuous path in the x-y plane constrained by physical laws and operational requirements. From the Model of trajectories, we extract, and formally prove, high level properties that can serve as a framework to analyze conflict scenarios. We use the Airborne Information for Lateral Spacing (AILS) alerting algorithm as a case study of our approach.
    Keywords: Computer Programming and Software
    Type: NASA/TM-2001-210864 , L-18083 , NAS 1.15:210864
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 6
    facet.materialart.
    Unknown
    Theorem Proving In Higher Order Logics (2002)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: The TPHOLs International Conference serves as a venue for the presentation of work in theorem proving in higher-order logics and related areas in deduction, formal specification, software and hardware verification, and other applications. Fourteen papers were submitted to Track B (Work in Progress), which are included in this volume. Authors of Track B papers gave short introductory talks that were followed by an open poster session. The FCM 2002 Workshop aimed to bring together researchers working on the formalisation of continuous mathematics in theorem proving systems with those needing such libraries for their applications. Many of the major higher order theorem proving systems now have a formalisation of the real numbers and various levels of real analysis support. This work is of interest in a number of application areas, such as formal methods development for hardware and software application and computer supported mathematics. The FCM 2002 consisted of three papers, presented by their authors at the workshop venue, and one invited talk.
    Keywords: Computer Programming and Software
    Type: NASA/CP-2002-211736 , NAS 1.55:211736 , L-18211 , Track B Proceedings of the 15th International Conference on Theorem Proving In Higher Order Logics: TPHOLs 2002; Aug 20, 2002 - Aug 23, 2002; Hampton, VA; United States|Formalising Continuous Mathematics: FCM 2002; Aug 19, 2002; Hampton, VA; United States
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 7
    facet.materialart.
    Unknown
    Design and Application of Strategies/Tactics in Higher Order Logics (2003)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: This Proceedings includes both a paper from the implementors of PVS providing guidance for PVS strategy writers and a tutorial on PVS strategy writing distilled from the experience of three PVS users who have written extensive sets of PVS user strategies. Following these are three full papers from the higher-order logic theorem proving community that discuss PVS strategies to enhance arithmetic and other interactive reasoning in PVS; implementing first-order tactics in higher-order provers; and a proposed technique for specifying small step semantics that can be used in multiple higher order logic theorem provers, with illustrations from both Coq and PVS. The Proceedings concludes with three position papers for a panel session that discuss three settings in which development of PVS strategies is worth while.
    Keywords: Computer Programming and Software
    Type: NASA/CP-2003-212448 , NAS 1.55:212448 , L-18328 , STRATA 2003: First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics; Sep 08, 2003; Rome; Italy
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 8
    facet.materialart.
    Unknown
    Explicit Substitutions and All That (2000)
    In:  CASI
    Details
    Publication Date: 2019-07-10
    Description: Explicit substitution calculi are extensions of the Lambda-calculus where the substitution mechanism is internalized into the theory. This feature makes them suitable for implementation and theoretical study of logic-based tools such as strongly typed programming languages and proof assistant systems. In this paper we explore new developments on two of the most successful styles of explicit substitution calculi: the lambda(sigma)- and lambda(s(e))-calculi.
    Keywords: Computer Programming and Software
    Type: NASA/CR-2000-210621 , ICASE-2000-45 , NAS 1.26:210621
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 9
    facet.materialart.
    Unknown
    An Overview of SAL (2000)
    In:  CASI
    Details
    Publication Date: 2019-07-10
    Description: To become practical for assurance, automated formal methods must be made more scalable, automatic, and cost-effective. Such an increase in scope, scale, automation, and utility can be derived from an emphasis on a systematic separation of concerns during verification. SAL (Symbolic Analysis Laboratory) attempts to address these issues. It is a framework for combining different tools to calculate properties of concurrent systems. The heart of SAL is a language, developed in collaboration with Stanford, Berkeley, and Verimag for specifying concurrent systems in a compositional way. Our instantiation of the SAL framework augments PVS with tools for abstraction, invariant generation, program analysis (such as slicing), theorem proving, and model checking to separate concerns as well as calculate properties (i.e., perform, symbolic analysis) of concurrent systems. We. describe the motivation, the language, the tools, their integration in SAL/PAS, and some preliminary experience of their use.
    Keywords: Computer Programming and Software
    Type: Lfm2000: Fifth NASA Langley Formal Methods Workshop; NASA/CP-2000-210100
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...