Results for 'Manfred Kerber Michael Kohlhase'

1000+ found
Order:
  1.  14
    Reasoning Without Believing: On the Mechanisation of Presuppositions and Partiality.Manfred Kerber & Michael Kohlhase - 2012 - Journal of Applied Non-Classical Logics 22 (4):295 - 317.
    (2012). Reasoning without believing: on the mechanisation of presuppositions and partiality. Journal of Applied Non-Classical Logics: Vol. 22, No. 4, pp. 295-317. doi: 10.1080/11663081.2012.705962.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  2.  84
    A Tableau Calculus for Partial Functions.Manfred Kerber Michael Kohlhase - unknown
    Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using a three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. We solve this (...)
    Translate
      Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  3. A Mechanization of Strong Kleene Logic for Partial Functions.Manfred Kerber Michael Kohlhase - unknown
    Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. We solve this problem (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  4.  5
    Interpreting Negatives in Discourse.Michael Kohlhase & Mandy Simons - unknown
    Michael Kohlhase and Mandy Simons. Interpreting Negatives in Discourse.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  5. Spreadsheet Interaction with Frames: Exploring a Mathematical Practice.Michael Kohlhase & Andrea Kohlhase - unknown
    Since Mathematics really is about what mathematicians do, in this paper, we will look at the mathematical practice of framing , in which an object of interest is viewed in terms of well-understood mathematical structures. The new perspective not only allows to deepen the understanding of e resp. object, it also facilitates new insights. We propose a model for framing in the context of theory graphs, and show how framing can be exploited to enhance the interaction with MKM systems. We (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  6.  14
    Reexamining the MKM Value Proposition: From Math Web Search to Math Web Research.Michael Kohlhase & Andrea Kohlhase - unknown
    The interest of the field of Mathematical Knowledge Management is predicated on the assumption that by investing into markup or formalization of mathematical knowledge, we can reap benefits in managing (creating, classifying, reusing, verifying, and finding) mathematical theories, statements, and objects. This global value proposition has been used to motivate the pursuit of technologies that can add machine support to these knowledge management tasks. But this (rather naive) technology-centered motivation takes a view merely from the global (macro) perspective, and almost (...)
    Direct download  
     
    Export citation  
     
    My bibliography  
  7. Extending OpenMath with Sequences.Fulya Horozal, Florian Rabe & Michael Kohlhase - unknown
    Sequences play a great role in mathematical communication. In mathematical notation, we use sequence ellipsis (. . . ) to denote "obvious" sequences like 1, 2, . . . , 7, and in conceptualizations sequence constructors like (i 2+1) i∈N. Furthermore, sequences have a prominent role as argument sequences of flexary functions. While the former cases can adequately be represented and reasoned about as domain objects in Open- Math and MathML, argument sequences are at the language level, and can only (...)
     
    Export citation  
     
    My bibliography  
  8. Adaptation of Notations in Living Mathematical Documents.Michael Kohlhase - unknown
    Notations are central for understanding mathematical discourse. Readers would like to read notations that transport the meaning well and prefer notations that are familiar to them. Therefore, authors optimize the choice of notations with respect to these two criteria, while at the same time trying to remain consistent over the document and their own prior publications. In print media where notations are fixed at publication time, this is an over-constrained problem. In living documents notations can be adapted at reading time, (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  9. A Mechanization of Sorted Higher-Order Logic Based on the Resolution Principle.Michael Kohlhase - unknown
    The usage of sorts in first-order automated deduction has brought greater conciseness of representation and a considerable gain in efficiency by reducing the search spaces involved. This suggests that sort information can be employed in higher-order theorem proving with similar results.
    Translate
     
     
    Export citation  
     
    My bibliography  
  10. What You Understand is What You Get: Assessment in Spreadsheets.Michael Kohlhase - unknown
    Spreadsheets are heavily employed in administration, financial forecasting, education, and science because of their intuitive, flexible, and direct approach to computation. In previous work we have studied how an explicit representation of the background knowledge associated with the spreadsheet can be exploited to alleviate usability problems with spreadsheet-based applications. The SACHS system implements this approach to provide a semantic help system for DCS, an Excelbased financial controlling system.
    No categories
    Translate
     
     
    Export citation  
     
    My bibliography  
  11. Cdmtcs.Michael Kohlhase - unknown
    In the last two decades, the World Wide Web has become the universal, and — for many users — main information source. Search engines can efficiently serve daily life information needs due to the enormous redundancy of relevant resources on the web. For educational — and even more so for scientific information needs, the web functions much less efficiently: Scientific publishing is built on a culture of unique reference publications, and moreover abounds with specialized structures, such as technical nomenclature, notational (...)
    Translate
      Direct download  
     
    Export citation  
     
    My bibliography  
  12. Capturing the Content of Physics: Systems, Observables, and Experiments.Michael Kohlhase - unknown
    We present a content markup language for physics realized by extending the OMDoc format by an infrastructure for the principal concepts of physics: observables, physical systems, and experiments.
     
    Export citation  
     
    My bibliography  
  13. Towards Mkm in the Large: Modular Representation and Scalable Software Architecture.Michael Kohlhase - unknown
    MKM has been defined as the quest for technologies to manage mathematical knowledge. MKM “in the small” is well-studied, so the real problem is to scale up to large, highly interconnected corpora: “MKM in the large”. We contend that advances in two areas are needed to reach this goal. We need representation languages that support incremental processing of all primitive MKM operations, and we need software architectures and implementations that implement these operations scalably on large knowledge bases. We present instances (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  14. Higher-Order Multi-Valued Resolution.Michael Kohlhase - 1999 - Journal of Applied Non-Classical Logics 9 (4):455-477.
    ABSTRACT This paper introduces a multi-valued variant of higher-order resolution and proves it correct and complete with respect to a variant of Henkin's general model semantics. This resolution method is parametric in the number of truth values as well as in the particular choice of the set of connectives (given by arbitrary truth tables) and even substitutional quantifiers. In the course of the completeness proof we establish a model existence theorem for this logical system. The work reported in this paper (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  15. Scripting Documents with XQuery: Virtual Documents in TNTBase.Michael Kohlhase - unknown
    This paper introduces the concept of Virtual Documents and its prototypical realization in our TNTBase system, a versioned XML database. VDs integrate XQuery-based computational facilities into documents like JSP/PHP do for relational queries. We view the integration of computation in documents as an enabling technology and evaluate it on a handfull of real-world use cases.
    No categories
    Translate
     
     
    Export citation  
     
    My bibliography  
  16.  67
    Notations for Living Mathematical Documents.Michael Kohlhase - unknown
    Notations are central for understanding mathematical discourse. Readers would like to read notations that transport the meaning well and prefer notations that are familiar to them. Therefore, authors optimize the choice of notations with respect to these two criteria, while at the same time trying to remain consistent over the document and their own prior publications. In print media where notations are fixed at publication time, this is an over-constrained problem. In living documents notations can be adapted at reading time, (...)
    Translate
      Direct download  
     
    Export citation  
     
    My bibliography  
  17. Computing Parallelism in Discourse.Michael Kohlhase - unknown
    Both Higher-Order Uni cation approaches to In linguistic theories on discourse coherence Kehler, discourse semantics Dalrymple et al., 1991; Shieber et.
     
    Export citation  
     
    My bibliography  
  18. A Resolution Calculus for Presuppositions.Michael Kohlhase - unknown
    The semantics of everyday language and the semantics..
    No categories
    Translate
     
     
    Export citation  
     
    My bibliography  
  19. Transforming the Arχiv to XML.Michael Kohlhase - unknown
    We describe an experiment of transforming large collections of L ATEX documents to more machine-understandable representations. Concretely, we are translating the collection of scientific publications of..
    No categories
    Translate
     
     
    Export citation  
     
    My bibliography  
  20. Higher{Order Coloured Uni Cation and Natural Language Semantics.Claire Gardent & Michael Kohlhase - unknown
    In this paper, we show that Higher{Order Coloured Uni cation { a form of uni cation developed for automated theorem proving { provides a general theory for modeling the interface between the interpretation process and other sources of linguistic, non semantic information. In particular, it provides the general theory for the Primary Occurrence Restriction which (Dalrymple et al., 1991)'s analysis called for.
    Translate
     
     
    Export citation  
     
    My bibliography  
  21.  33
    Higher-Order Semantics and Extensionality.Christoph Benzmüller, Chad E. Brown & Michael Kohlhase - 2004 - Journal of Symbolic Logic 69 (4):1027 - 1088.
    In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of (machine-oriented) higher-order calculi with respect to these model classes.
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  22. Reqdoc.Sty: Semantic Markup for Requirements Specification Documents.Michael Kohlhase - unknown
    This package provides an infrastructure for semantically enhanced requirements specifications used in software engineering. This allows to embed structural information into documents that can be used by semantic document managment systems e.g. for management of change and requirements tracing.
    Direct download  
     
    Export citation  
     
    My bibliography  
  23. System Description: Analytica 2.Michael Kohlhase - unknown
    The Analytica system is a theorem proving system for 19 th century mathematics written on top of the Mathematica computer algebra system. It was developed in the early 1990’s by X. Zhao and E. Clarke and has since been dormant. We describe recent work to resurrect the theorem prover and port it to newer versions of Mathematica. The new system Analytica 2 can still prove the same theorems, but has been significantly cleaned up. The code has been restructured and documented, (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  24. An Exploration in the Space of Mathematical Knowledge.Michael Kohlhase - unknown
    Although knowledge is a central topic for MKM there is little explicit discussion on what ‘knowledge’ might actually be. There are specific intuitions about form and content of knowledge, about its structure, and epistemological nature that shape the MKM systems, but a conceptual model is missing. In this paper we try to rationalize this discussion to give MKM a firmer footing, to start a discussion among MKM researchers and help relate the MKM intuitions and discourses to other communities. Starting from (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  25. System Description: { A Higher-Order Theorem Prover?Michael Kohlhase - manuscript
    Thus, despite the di culty of higher-order automated theorem proving, which has to deal with problems like the undecidability of higher-order uni - cation (HOU) and the need for primitive substitution, there are proof problems which lie beyond the capabilities of rst-order theorem provers, but instead can be solved easily by an higher-order theorem prover (HOATP) like Leo. This is due to the expressiveness of higher-order Logic and, in the special case of Leo, due to an appropriate handling of the (...)
     
    Export citation  
     
    My bibliography  
  26. Physml.Sty: An Infrastructure for Marking Up Physml in Tex/L.Michael Kohlhase - unknown
    The physml packge allows mark up PhysML structures in L ATEX documents that can be harvested by automated tools or exported to PDF, while..
    No categories
    Translate
     
     
    Export citation  
     
    My bibliography  
  27. CPoint: Dissolving the Author's Dilemma.Michael Kohlhase - unknown
    Automated knowledge management techniques critically depend on the availability of semantically enhanced documents which are hard to come by in practice. Starting from a detailed look at the motivations of users to produce semantic data, we argue that the authoring problem experienced by MKM is actually an author’s dilemma. An analysis of the content authoring process suggests that the dilemma can partially be overcome by providing authoring tools like invasive editors aimed specifically at supporting the content creator. We present the (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  28. A Search Engine for Mathematical Formulae.Michael Kohlhase - unknown
    We present a search engine for mathematical formulae. The MathWebSearch system harvests the web for content representations (currently MathML and OpenMath) of formulae and indexes them with substitution tree indexing, a technique originally developed for accessing intermediate results in automated theorem provers. For querying, we present a generic language extension approach that allows constructing queries by minimally annotating existing representations. First experiments show that this architecture results in a scalable application.
    Translate
     
     
    Export citation  
     
    My bibliography  
  29. A Foundational View on Integration Problems.Michael Kohlhase - unknown
    The integration of reasoning and computation services across system and language boundaries has been mostly treated from an engineering perspective. In this paper we take a foundational point of view. We identify the following form of integration problems: an informal (mathematical; i.e, logically underspecified) specification has multiple concrete formal implementations between which queries and results have to be transported. The integration challenge consists in dealing with the implementation-specific details such as additional constants and properties. We pinpoint their role in safe (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  30. Compensating the Computational Bias of Spreadsheets with MKM Techniques.Michael Kohlhase - unknown
    Spreadsheets are mathematical documents that are heavily employed in administration, financial forecasting, education, and science because of their intuitive, flexible, and direct approach to computation. In this paper we show that spreadsheets are interesting applications for MKM techniques which can alleviate usability and maintenance problems as spreadsheet-based applications grow evermore complex and longlived. We present the software and information architecture of a semantic enhancement of MS Excel spreadsheets that aims at compensating the computational bias in spreadsheets.
    Translate
     
     
    Export citation  
     
    My bibliography  
  31. Semantic Transparency in User Assistance Systems.Michael Kohlhase - unknown
    transparency as a user interface property that enables giving appropriate help. We explicate this notion in document player applications found in office suites, for example. Moreover, we show how semantic transparency can be strengthened when the underlying software is complemented by a semantic ally system. The approach consists in illustrating existing software semantically. We present some semantic extensions of office applications as examples. We also deaction task. scribe how the semantic transparency approach allows the..
    No categories
    Translate
     
     
    Export citation  
     
    My bibliography  
  32.  90
    Sref.Sty: Semantic Crossreferencing in L.Michael Kohlhase - unknown
    The sref packge is part of the STEX collection, a version of TEX/L..
    Translate
      Direct download  
     
    Export citation  
     
    My bibliography  
  33. Model Generation for Discourse Representation Theory.Michael Kohlhase - unknown
    Semantic analysis, – inference on the basis of semantic information and world knowledge – still is largely uncharted territory in dy- (3) namic semantics. It is needed, among other things, for the reconstruction of linguistically unspecified parts of the discourse or for restricting ambiguities introduced by prior analysis processes, i.e.
    Translate
     
     
    Export citation  
     
    My bibliography  
  34. Higher-Order Automated Theorem Proving.Michael Kohlhase - unknown
    The history of building automated theorem provers for higher-order logic is almost as old as the field of deduction systems itself. The first successful attempts to mechanize and implement higher-order logic were those of Huet [13] and Jensen and Pietrzykowski [17]. They combine the resolution principle for higher-order logic (first studied in [1]) with higher-order unification. The unification problem in typed λ-calculi is much more complex than that for first-order terms, since it has to take the theory of αβη-equality into (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  35. Quantifiers and Big Operators in OpenMath.James H. Davenport & Michael Kohlhase - unknown
    The effort to align MathML 3 and OpenMath has led to a realisation that (pragmatic) MathML’s condition and domainofapplication elements, when used with quantifiers, do not have a neat expression in OpenMath. This paper analyzes the situation focusing on quantifiers and proposes a solution, via six new symbols. Two of them fit completely within the existing OpenMath structure, and we place them in the associated quant3 CD. The others require a generalization of OMBIND. We also propose, logically separately but in (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  36. Unification in a A-Calculus with Intersection Types.Michael Kohlhase & Frank Pfenning - unknown
    We propose related algorithms for unification and constraint simplification in }F’&, a refinement of the simply-typed A-calculus with subtypes and bounded intersection types. }F""’ is intended as the basis of a logical framework in order to achieve more succinct and declarative axiomatiza-.
    No categories
     
    Export citation  
     
    My bibliography  
  37. Prototyping a Browser for a Listed Buildings Database with Semantic MediaWiki.Michael Kohlhase - unknown
    Listed buildings, even if they are not top landmarks, are increasingly attracting visitors. People express interest in hidden gems in their neighborhood or along their travel itinerary, and in the history of the building they live in. All required data has been meticulously collected by the offices for historical monuments but is not flexibly accessible. In Bremen, the database of buildings (with location, map of the estate, construction history, architect, photos) is searchable and browsable online3, but that only helps users (...)
    No categories
    Translate
     
     
    Export citation  
     
    My bibliography  
  38. Modeling Task Experience in User Assistance Systems.Andrea Kohlhase & Michael Kohlhase - unknown
    One of the major issues for user assistance systems consists of “providing help at an appropriate level”. In this paper we analyze the problem of modeling task experience — a prerequisite for provisioning adequate help. In contrast to level-based approaches we propose an ontology-based model, which allows fine-grained modeling of task experience using the concepts of the task domain as granules. The model is semantic in the sense that it allows to take advantage of the relations between concepts to provide (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  39. Communities of Practice in MKM: An Extensional Model.Michael Kohlhase - unknown
    We explore the social context of mathematical knowledge: Even though, the community of mathematicians may look homogeneous from the outside, it is actually structured into various sub-communities that differ in preferred notations, the choice of basic assumptions, or e.g. in the choice of motivating examples. We contend that we cannot manage mathematical knowledge for human recipients if we do not take these factors into account. As a basis for a future extension of MKM systems, we analyze the social context of (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  40. TNTBase: A Versioned Storage for XML.Vyacheslav Zholudev & Michael Kohlhase - unknown
    Version Control systems like CVS and Subversion have transformed collaboration workflows in software engineering, and made possible the globally distributed project teams we know from the Open Source Phenomenon. On the other hand, XML is coming of age as a basis for document formats, and even though XML as a text-based format is amenable to version control in principle, the fact that version control systems work on files makes difficult the integration of fragment access techniques like XPath, XQuery that are (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  41. Towards an Atlas of Formal Logics.Michael Kohlhase & Kristina Sojakova - unknown
    LF has been designed as a meta-logical framework to represent logics, and has become a standard tool for studying properties of logics. Building on the newly introduced module system for LF, we present the nucleus of an integrated and structured development of the syntax, semantics, and proof theory of logics, and of the relations between those logics. The methodology is chosen so that it will scale to an atlas for the zoo of logics currently used in reasoning systems, and the (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  42. Semantic Knowledge Management for Education.Michael Kohlhase - unknown
    ‘Semantic technologies’ are touted as the next big wave in Educational Technology and as the solution to many problems in this arena. Interdisciplinary work between the fields of Knowledge Management (KM) and Educational Technology (ET) is booming. But the crop of actual systems and semantically enhanced learning objects is still meager, maybe KM and EL they are lacking a consensus on the underlying notions e.g. of ‘semantics’, yielding specific problems in their interplay. In this paper we take a look at (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  43. Semantics of Openmath and Mathml.Michael Kohlhase - unknown
    Even though OpenMath has been around for more than 10 years, there is still confusion about the “semantics of OpenMath”. As the upcoming MathML3 recommendation will semantically base Content MathML on OpenMath Objects, this question becomes more pressing. One source of confusions about OpenMath semantics is that it is given on two levels: a very weak algebraic semantics for expression trees, which..
    Translate
     
     
    Export citation  
     
    My bibliography  
  44. Towards a Dynamic Type Theory.Michael Kohlhase - unknown
    Over the past few years, there have been a series of attempts Zee89, GS90, EK95, Mus94, KKP95] to combine the Montagovian type theoretic framework Mon74] with dynamic approaches, such as DRT Kam81]. The motivation for these developments is to obtain a general logical framework for discourse semantics that combines compositionality and dynamic binding.
     
    Export citation  
     
    My bibliography  
  45. Unifying Math Ontologies: A Tale of Two Standards.James H. Davenport & Michael Kohlhase - unknown
    One of the fundamental and seemingly simple aims of mathematical knowledge management (MKM) is to develop and standardize formats that allow to “represent the meaning of the objects of mathematics”. The open formats OpenMath and MathML address this, but differ subtly in syntax, rigor, and structural viewpoints (notably over calculus). To avoid fragmentation and smooth out interoperability obstacles, effort is under way to align them into a joint format OpenMath/MathML 3. We illustrate the issues that come up in such an (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  46. A Better Role System for OpenMath.Michael Kohlhase - unknown
    OpenMath is a standard for the representation and communication of mathematical objects, which are built up from symbols and variables using applications, binding expressions, and key-value attributions. OpenMath2 introduced a set of symbol roles that can be specified in content dictionaries to restrict the occurrences of the respective symbols. This yields a simple, high-level notion of well-formed objects. While this system is appealing in its simplicity, the definition of wellformedness is purely extensional without an intuitive or formal condition that distinguishes (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  47.  21
    For Mathematical Documents.Michael Kohlhase - unknown
    The OMDoc (Open Mathematical Documents) format is a content markup scheme for (collections of) mathematical documents including articles, textbooks, interactive books, and courses. OMDoc also serves as the content language for agent communication of mathematical services on a mathematical software bus.
    No categories
    Translate
      Direct download  
     
    Export citation  
     
    My bibliography  
  48. Towards Collaborative Content Management and Version Control for Structured Mathematical Knowledge.Michael Kohlhase - unknown
    We propose an infrastructure for collaborative content management and version control for structured mathematical knowledge. This will enable multiple users to work jointly on mathematical theories with minimal interference. We describe the API and the functionality needed to realize a cvs-like version control and distribution model. This architecture extends the cvs architecture in two ways, motivated by the specific needs of distributed management of structured mathematical knowledge on the Internet. On the one hand the one-level client/server model of cvs is (...)
    Translate
     
     
    Export citation  
     
    My bibliography  
  49.  28
    MathWebSearch 0.4 A Semantic Search Engine for Mathematics.Michael Kohlhase - unknown
    We present a search engine for mathematical formulae. The MathWebSearch system harvests the web for content representations of formulae and indexes them with substitution tree indexing. In version 0.4 we have parallelized and distributed the search server and augmented the web interface with a new JavaScript-based visual editor for content math formulae. Furthermore, we have extended the query language by generalization, variants, unification, and text search facilities, which can also be mixed. Our experiments show that this architecture results in a (...)
    Translate
      Direct download  
     
    Export citation  
     
    My bibliography  
  50.  34
    Inference and Computational Semantics.Patrick Blackburn & Michael Kohlhase - 2004 - Journal of Logic, Language and Information 13 (2):117-120.
1 — 50 / 1000