Abstracts
Co-Synthesis of New Complex Selection Algorithms and their Human Comprehensible XML Documentation
In this paper, an approach for program and algorithm synthesis within a higher-order framework is presented that allows us to generate new algorithm structures together with readable documentation which enable users to conveniently inspect the results of this synthesis process. The synthesis approach is based on feature graphs as a higher-order data type for specifying synthesis types like proof terms, theorems and document types. The document synthesis method uses constructive reasoning about a user-defined knowledge base to synthesise documents from metaobjects which are composed of diagrams, and references to articles, theorems and algorithms. The data format used for reasoning is a variant of XML syntax and thus enables the organisation of comprehensive knowledge in XML repositories and the conversion of document terms into LaTeX, PDF or XHTML documents which can be displayed by browsers.
This framework has been applied for the automated synthesis of several new selection algorithms and their documentation. As one new result, an algorithm that proves selecting the 4th element of 24 elements needs at most 34 comparisons was synthesised using 50 seconds CPU time on an AMD Athlon 3200. The correctness of the synthesised algorithm was manually checked. It improves the known upper bounds for the specific selection problems. The running time for synthesis is several orders of magnitude more efficient than comparative approaches.
Workshop on Empirically Successful Automated Reasoning in Higher-Order Logics ESHOL 2005, Montego Bay, Jamaica, December 2, 2005
Knowledge modeling for evolutionary program synthesis
This paper proposes a multi-layer methodology – called SEAMLESS – for the design of knowledge-based program synthesis systems within the logic programming paradigm. The intent is to provide an integrated logical framework for modeling the different kinds of knowledge involved during program synthesis processes and a workbench of inference-based generic tools for the constructive solution of knowledge acquisition and program synthesis tasks. As major requirements, evolutionary synthesis processes, the re-usability of knowledge chunks, and multiple views should be facilitated. The approach depends upon the definition of hierarchically organized abstraction layers. It is a combination of abstract data types and typed predicate logic used for domain modeling. Metatheories allow for the specification of generic problem solving knowledge and generic tactics in a domain independent way. The interaction between theories and abstract representations is realized by interface definitions. Our approach borrows concepts from object-oriented programming to structure the comprehensive theory by frame-like types and to support inheritance. Meta-programming techniques provide language facilities to describe the dynamic change of theories and allow reasoning about theories. Based on this theoretical foundation, we implemented a knowledge based program synthesis system and applied it to the discovery of a non-trivial mathematical algorithm.
Appeared in:
Proceedings of the 8th International Symposium on Methodologies for Intelligent Systems
pages 17 - 30. Oak Ridge National Laboratory, N00014-94-1-0799, 1994.
Knowledge Mediation in the WWW Based on Labelled DAGs with Attached Constraints
his paper introduces a framework where the semantic access to Web resources is realised by a mediator module. Users can express their knowledge needs using the terms of a shared ontology without taking into account context-specific locations, encodings, and vocabulary. Integration among shared ontologies and Web meta data descriptions is achieved by inserting an intelligent meta-level layer using lifting rules. Lifting rules can be used to automatically decompose semantic information needs into concrete information requests. Wrapper and facilitator agents are used to find suitable information on the Web.
Labelled directed acyclic graphs (DAGs) allow a natural modelling of syntactical, structural and semantic properties of standardised XML Web data meta data, and ontologies, and their operations. However, graph-based data models are only a first step towards intelligent tools for automated knowledge extraction from the WWW. Planning and design synthesis of technical systems involve dealing with interacting constraints, imposed by selected tasks, such as cost or compatibility constraints, or general constraints.
As a step to cope with these requirements, a novel approach combining constraint processing and reasoning with Web (meta-)data is presented. Canonical graphterms are used for the encoding of labelled DAGs, which are embedded into constraint logic formulas, thus representing Web (meta-)data and ontologies. Graph rewriting and application of the built-in reasoning facilities such as matching, unification, subsumption and constraint solving of a constraint-logic language can then be used to efficiently automate mediation tasks.
Appeared in:
Electronic Transactions on Artificial Intelligence, Vol 5 (2001), Section D
Errata to »Selecting the top three elements« by M. Aigner: A Result of a computer assisted proof search.
Based on negative results of an attempt to re-establish the known results for the combinatorial functions U_3(n), V_3(n) and W_3(n), an anomaly of these mappings that occurs at certain arguments was detected by a computer-assisted proof search. So far, the corrected values of the numbers U_3(23) and V_3(22) are proven. Except for finitely many n, no change is made to the published formulas for the functions U_3(n), V_3(n) and W_3(n).
Appeared in:
Discrete Applied Mathematics 41:131--137, 1992
Efficient knowledge based reasoning with transitive DAG's
This paper sketches the efficient term representation and implementation of transitive, directed, acyclic graphs (DAGs), their operations and behavioural equivalences within an order-sorted logic, where sorts and subsorts are associated with concepts and subconcepts. Semantical correctness can be shown. As a major new result, a well-founded term ordering was defined which proves the existence of unique term representatives for semantically identical objects and classes of isomorphic DAGs. Moreover, canonical forms for objects are constructed from a single arbitrary term representative of the class by replacing constants with variables, ie. generalisation. Employing the proposed repesentational format, set theoretic decision, construction and transformation procedures on transitive DAGs and its classes are implemented in an efficient way by basic operations in logic programming, ie. term rewriting, instantiation, generalization, subsumption, unification and anti-unification. Hence, knowledge on transitive DAGs may be specified in an extended order-sorted logic and can be retrieved efficiently by inference based methods. Uniform logic based proof, program synthesis or theory formation procedures can be used to perform inductive and deductive reasoning on DAGs efficiently.
Appeared in:
Proceedings of the International KRUSE Symposium, Knowledge
Retrieval, Use and Storage for Efficiency 1995
Speed-up transformations of logic programs by abstraction and learning
This paper presents a formal framework for the automatic transformation of inefficient generate and test programs into equivalent programs by learning from the proofs of example queries. In the resulting program the search is guided by strategies based on abstracted proof traces obtained from the interpretation of example computations. Strategies are incrementally improved in an iterative process by a method for theory formation. For the task of theory formation we develop a logic based method. It operates on a triple, consisting of a set of features augmented with taxonomic relations, a sequence of positive and negative facts and a set of disjunctive hypotheses, which can also be the empty set. This triple is transformed into a set of disjunctive hypotheses which implies all of the positive facts, but none of the negative facts and the number of hypotheses is minimal. Hypotheses are constructed from facts by abstraction.
Appeared in:
K.K. Lau and T. Clement, editors, Logic Program Synthesis and Transformation, pages 167-182. Springer Verlag, 1992
Knowledge Based Methods for the Synthesis of Mathematical Proofs: A Combinatorial Application
In the thesis Knowledge Based Methods for the Synthesis of Mathematical Proofs: A Combinatorial Application, a comprehensive logical framework for the formalization of problem solving in combinatorial domains is devised. Combinatorial problem solving is regarded as a program synthesis task. Thus, combinatorial problems are solved by deriving constructive proofs of goal specification formulas as suggested by the »proofs as programs« paradigm. The framework integrates the representation, the acquisition and the application of mathematical knowledge.
Our model provides a layered structuring of the different kinds of knowledge involved in synthesis tasks. The objects on each layer are represented by terms, while there properties are specified by logical formulas. For describing properties of domain objects, our specification language provides syntactical features which allow to express taxonomical concepts and uncertain knowledge explicitely. As an application of the representation framework, we present operational logical specifications of posets, their operations and properties. Thus, posets can be encoded by terms. As a new result, the existence of canonical terms for posets and for classes of isomorphic posets is proven by defining an adequate term ordering. Furthermore, it is shown that class representatives are easily constructable from ground terms by replacing constants with variables.
We assume that correct domain-independant problem-solving tactics may be derived by proving metatheorems. Decomposition theories which reflect generic structures common to different domains are introduced. Hence, domains can be represented as annotated decomposition theories. To distinguish strategic knowledge, relationships such as behavioural equivalence, reduction, and generalization are defined between sets of formulas. The use of decomposition theories faciliates the application of design tactics to program synthesis. We formalize a design tactic for decomposition theories which is based on the computational paradigm of »divide-and-conquer«. Its correctness is proven by applying the principle of structural induction. This result reduces the proof of goal specifications to the construction of an adequate generalization and the definition of a corresponding function. They are constructed as follows: proven instances of the goal specification are transformed into a general description by an incremental method for theory formation. The proofs of the goal specifications exploit the different kinds of knowledge given by an extended decomposition theory. These formalizations were successfully employed to develop a knowledge based program synthesis system, called ASK (Acquiring Synthesis Knowledge). Goal specifications can be proven with respect to dynamically created and modified theories. Synthesized knowledge is re-used for further proof processes.
The viability of the methods as well as the performance of the implementation are examined empirically in the case of the »selection problem«. The selection problem asks for a formula, which predicts the minimum number of comparisons needed to determine the i-th largest element of a totally ordered set in the worst-case. The formula is proven for little values of i (i = 1,2,3). Known mathematical results concerning the selection problem are reproduced in a uniform way. Additionally, we derive new numbertheoretic results and extends them by a numbertheoretic hypothesis. Especially, employing the system ASK interactively a counter-example to a ``proven'' theorem was generated and published.
Written in German. Appeared in:
DISKI