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
  • 1
    Electronic Resource
    Electronic Resource
    Social and Semiotic Analyses for Theorem Prover User Interface Design 1 (1999)
    Springer
    Formal aspects of computing 11 (1999), S. 272-301 
    Details
    ISSN: 1433-299X
    Keywords: Keywords: User interface design; Theorem proving; Semiotics; Sociology; CSCW; Algebraic specification; Narratology; Algebraic semiotics
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract. We describe an approach to user interface design based on ideas from social science, narratology (the theory of stories), cognitive science, and a new area called algebraic semiotics. Social analysis helps to identify certain roles for users with their associated requirements, and suggests ways to make proofs more understandable, while algebraic semiotics, which combines semiotics with algebraic specification, provides rigorous theories for interface functionality and for a certain technical notion of quality. We apply these techniques to designing user interfaces for a distributed cooperative theorem proving system, whose main component is a website generation and proof assistance tool called Kumo. This interface integrates formal proving, proof browsing, animation, informal explanation, and online background tutorials, drawing on a richer than usual notion of proof. Experience with using the interface is reported, and some conclusions are drawn.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/s001650050051
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Electronic Resource
    Electronic Resource
    Software component search (1996)
    Springer
    Journal of systems integration 6 (1996), S. 93-134 
    Details
    ISSN: 1573-8787
    Keywords: Component search ; retrieval ; software library ; reuse ; computer aided prototyping
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract An important problem in software development is to make better use of software libraries by improving the search and retrieval process, that is, by making it easier to find the few components you may want among the many you do not want. This paper suggests some ideas to improve this process: (1) Associate analgebraic specification with each software component; these specifications should include complete syntactic information, but need have onlypartial semantic information. (2) User queries consist of syntactic declarations plus results forsample executions. (3) User queries may be posed in standard programming notation, which is then automatically translated into algebraic notation. (4) Search is organized asranked multi-level filtering, where each level yields aranked set of partial matches. (5) Early stages of filtering narrow the search space by using computationally simple procedures, such as checking that the number of types is adequate. (6) Middle levels may findpartial signature matches. (7) Pre-computedcatalogues (i.e., indexes) can speed up early and middle level filtering. (8) Semantic information is used in a final filter withterm rewriting, but complete verification is not attempted. (9) The series of filters is implementedincrementally, so as to backtrack to lower ranked components in case of failure. This approach avoids the need for complex theorem proving, and does not require any knowledge of algebraic specification from the user. Moreover, it does not require either specifications or queries to be complete or even fully correct, because it yields partial matches ranked by how well they fit the query. The paper concludes with a description of some preliminary experiments and some suggestions for further experiments.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF02262753
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 3
    facet.materialart.
    Unknown
    Order-sorted unification (1989)
    Elsevier
    Details
    Publication Date: 1989-10-01
    Print ISSN: 0747-7171
    Electronic ISSN: 1095-855X
    Topics: Computer Science , Mathematics
    Published by Elsevier
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    PAPER CURRENT
  • 4
    facet.materialart.
    Unknown
    Data, Schema, Ontology and Logic Integration (2005)
    Oxford University Press
    Details
    Publication Date: 2005-11-01
    Print ISSN: 1367-0751
    Electronic ISSN: 1368-9894
    Topics: Mathematics
    Published by Oxford University Press
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    PAPER CURRENT
  • 5
    facet.materialart.
    Unknown
    Modular algebraic specification of some basic geometrical constructions (1988)
    Elsevier
    Details
    Publication Date: 1988-12-01
    Print ISSN: 0004-3702
    Electronic ISSN: 1872-7921
    Topics: Computer Science
    Published by Elsevier
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    PAPER CURRENT
  • 6
    facet.materialart.
    Unknown
    Circular Coinduction (2001)
    In:  CASI
    Details
    Publication Date: 2013-08-29
    Description: Circular coinduction is a technique for behavioral reasoning that extends cobasis coinduction to specifications with circularities. Because behavioral satisfaction is not recursively enumerable, no algorithm can work for every behavioral statement. However. algorithms using circular coinduction can prove every practical behavioral result that we know. This paper proves the correctness of circular coinduction and some consequences.
    Keywords: Computer Programming and Software
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 7
    facet.materialart.
    Unknown
    Communication training for aircrews: A review of theoretical and pragmatic aspects of training program design (1987)
    In:  CASI
    Details
    Publication Date: 2019-06-28
    Description: This study is the final report of a project studying methods of communications training applicable to both civilian and military aviation personnel, including multiperson teams or single pilot fixed wing or rotary wing aircraft. A review is provided of a number of theories proposed as relevant for producing training materials for improved communications. Criteria are given for evaluating the applicability of training programs to the aviation environment, and these criteria are applied to United Airlines' Resources Management Training, as well as to a number of commercially available general purpose training programs. The report considers in detail assertiveness training and grid management training, examining their theoretical background and attempts made to validate their effectiveness. It was found that there are substantive difficulties in assessing the effectiveness of both training programs, as well as problems with the theories underlying them. However, because the aviation environment offers unique advantages for studying the effectiveness of communications training, recommendations are made on the design of appropriate training programs and on procedures that might be used to validate them.
    Keywords: AIR TRANSPORTATION AND SAFETY
    Type: NASA-CR-177459 , NAS 1.26:177459
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 8
    facet.materialart.
    Unknown
    Checklist interruption and resumption: A linguistic study (1987)
    In:  CASI
    Details
    Publication Date: 2019-06-28
    Description: This study forms part of a project investigating the relationships among the formal structure of aviation procedures, the ways in which the crew members are taught to execute them, and the ways in which thet are actually performed in flight. Specifically, this report examines the interactions between the performance of checklists and interruptions, considering both interruptions by radio communications and by other crew members. The data consists of 14 crews' performance of a full mission simulation of a higher ratio of checklist speech acts to all speech acts within the span of the performance of the checklist. Further, it is not number of interruptions but length of interruptions which is associated with crew performance quality. Use of explicit holds is also associated with crew performance.
    Keywords: AIR TRANSPORTATION AND SAFETY
    Type: NASA-CR-177460 , NAS 1.26:177460
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 9
    facet.materialart.
    Unknown
    How Effective Is Communication Training For Aircraft Crews (1992)
    In:  Other Sources
    Details
    Publication Date: 2019-07-12
    Description: Report surveys communication training for aircraft crews. Intended to alleviate problems caused or worsened by poor communication and coordination among crewmembers. Focuses on two training methods: assertiveness training and grid-management training. Examines theoretical background of methods and attempts made to validate their effectiveness. Presents criteria for evaluating applicability to aviation environment. Concludes communication training appropriate for aircraft crews.
    Keywords: LIFE SCIENCES
    Type: ARC-12329 , NASA Tech Briefs (ISSN 0145-319X); 16; 11; P. 120
    Format: text
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 10
    facet.materialart.
    Unknown
    Institution Morphisms (2001)
    In:  CASI
    Details
    Publication Date: 2019-07-10
    Description: Institutions formalize the intuitive notion of logical system, including both syntax and semantics. A surprising number of different notions of morphisim have been suggested for forming categories with institutions as objects, and a surprising variety of names have been proposed for them. One goal of this paper is to suggest a terminology that is both uniform and informative to replace the current rather chaotic nomenclature. Another goal is to investigate the properties and interrelations of these notions. Following brief expositions of indexed categories, twisted relations, and Kan extensions, we demonstrate and then exploit the duality between institution morphisms in the original sense of Goguen and Burstall, and the 'plain maps' of Meseguer, obtaining simple uniform proofs of completeness and cocompleteness for both resulting categories; because of this duality, we prefer the name 'comorphism' over 'plain map.' We next consider 'theoroidal' morphisms and comorphisims, which generalize signatures to theories, finding that the 'maps' of Meseguer are theoroidal comorphisms, while theoroidal morphisms are a new concept. We then introduce 'forward' and 'semi-natural' morphisms, and appendices discuss institutions for hidden algebra, universal algebra, partial equational logic, and a variant of order sorted algebra supporting partiality.
    Keywords: Cybernetics, Artificial Intelligence and Robotics
    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...