A5021113261- Logic, programming, and type systems
- Formal Methods in Verification
- Logic, Reasoning, and Knowledge
- Numerical Methods and Algorithms
- semigroups and automata theory
- Algorithms and Data Compression
- Polynomial and algebraic computation
- Advanced Database Systems and Queries
- Parallel Computing and Optimization Techniques
- Digital Filter Design and Implementation
- Coding theory and cryptography
- Low-power high-performance VLSI design
- Model-Driven Software Engineering Techniques
- Mathematics, Computing, and Information Processing
- Embedded Systems Design Techniques
- Intelligent Tutoring Systems and Adaptive Learning
- Computability, Logic, AI Algorithms
- Commutative Algebra and Its Applications
- Distributed and Parallel Computing Systems
- Semantic Web and Ontologies
- History and Theory of Mathematics
- Cellular Automata and Applications
- Software Testing and Debugging Techniques
- Advanced Algebra and Logic
- Teaching and Learning Programming
Johannes Kepler University of Linz
2012-2024
West University of Timişoara
2024
RISC Software (Austria)
1995-2021
Association for Symbolic Logic
1996-2015
Software Competence Center Hagenberg (Austria)
2009
Cornell University
1993-1998
Karlsruhe University of Education
1998
Masaryk University
1998
Utrecht University
1998
Heidelberg (Poland)
1998
The Theorema project aims at the development of a computer assistant for working mathematician. Support should be given throughout all phases mathematical activity, from introducing new concepts by definitions or axioms, through first (computational) experiments, formulation theorems, their justification an exact proof, application theorem as algorithm, until to dissemination results in form publication, build up bigger libraries certified content and like. This ambitious is exactly along...
Article Free Access Share on A generalization of the binary GCD algorithm Author: T. Jebelean View Profile Authors Info & Claims ISSAC '93: Proceedings 1993 international symposium Symbolic and algebraic computationAugust Pages 111–116https://doi.org/10.1145/164081.164102Online:01 August 1993Publication History 28citation794DownloadsMetricsTotal Citations28Total Downloads794Last 12 Months31Last 6 weeks4 Get Citation AlertsNew Alert added!This alert has been successfully added will be sent...
We present an algorithm that generates automatically (algebraic) invariant properties of a loop with conditionals. In the proposed program analysis is performed in order to transform code into form for which algebraic and combinatorial techniques can be applied obtain properties. These invariants are then used verifying partial correctness imperative programs Theorema system (www.theorema.org). The application method demonstrated few examples.
The execution times of several algorithms for computing the GCD arbitrary precision integers are compared. These known ones (Euclidean, binary, plus-minus), and improved variants these multidigit computation (Lehmer similar), as well new introduced by author: an Lehmer algorithm using two digits in partial consequence computation, a generation binary concept modular conjugates. last prove to be fastest all, giving speedup six eight over classical Euclidean scheme, best currently algorithms....
We study and implement concrete methods for the verification of both imperative as well functional programs in frame Theorema system. The distinctive features our approach consist automatic generation loop invariants (by using combinatorial algebraic techniques), conditions first-order logical formulae which do not refer to a specific model computation.
One important characteristic of environment re-search <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1</sup> is the handling very large amounts data, which can be only achieved by organizing it in a highly efficient way, particular keeping various indexing lists sorted way and maintaining them efficiently. Therefore sorting algorithms that are specifically tailored to situations occurring data acquisition, storage, maintenance crucial for...
In the context of constructive synthesis sorting algorithms, starting from specification problem (input and output conditions), proof existence a sorted tuple is performed inductively we design, implement, experiment with different techniques: First use back-chaining mechanism similar to Prolog engine for first order logic, in which meta-variables are used finding existential witnesses. overcome search space explosion, introduce various specific prove-solve methods theory tuples. For...
Algorithm certification or program verification have an increasing importance in the current technological landscape, due to sharp increase complexity of software and using systems high potential adverse effects case failure. For instance robots constitute a particular class that can present risks such failures. Sorting on other hand has growing area applications, ones where organizing huge data collections is critical, as for environmental applications. We experiment formal original version...
We present the systematic build-up in Theorema system of theory lists. This was carried out parallel with process synthesis some sorting algorithms same system. use appropriate induction principles for lists and we construct a collections properties which are necessary automatic algorithms. In contrast another version list system, is based on higher order logic uses sequence variables, our approach first predicate (which semi-decidable). opens way effective automation proofs, exploration...
We start from the set theory axioms and we represent sets by monotone lists (sorted without duplications). For this, define a representation function R its reverse S want to synthesize implementation of essential corresponding predicates functions over sets. Each synthesis starts as an inductive constructive proof which applies specific strategies inference rules. (by extracting proofs) five algorithms among two predicates: membership inclusion, three functions: union, intersection,...
The construction of a theory for binary trees is presented, based on the systematic exploration properties necessary proof-based synthesis and certification sorting algorithms trees. process computer supported, being realised in frame Theorema system, with some additional proofs Coq required algorithm certification. result consists 11 definitions, 3 axioms, more than 200 properties. Also, 5 are generated.
In the frame of our previous experiments for proof based synthesis sorting algorithms lists and binary trees, we employed certain special techniques which are able to generate multiple variants merging, by investigating all combinations auxiliary functions available composing objects (lists, respectively trees). The purpose this paper is describe technique results obtained. We present main principles application merging sorted trees into a one. Remarkably, requires nested recursion, an...