Search

Your search keyword '"Kerber, Manfred"' showing total 484 results
Start Over Author "Kerber, Manfred"

Refine your results

more »

more »

more »

more »
484 results on '"Kerber, Manfred"'

2. Applying the Isabelle Insider Framework to Airplane Security

Author

Kammüller, Florian and Kerber, Manfred

Subjects
Computer Science - Software Engineering, Computer Science - Logic in Computer Science
Abstract

Avionics is one of the fields in which verification methods have been pioneered and brought a new level of reliability to systems used in safety critical environments. Tragedies, like the 2015 insider attack on a German airplane, in which all 150 people on board died, show that safety and security crucially depend not only on the well functioning of systems but also on the way how humans interact with the systems. Policies are a way to describe how humans should behave in their interactions with technical systems, formal reasoning about such policies requires integrating the human factor into the verification process. In this paper, we report on our work on using logical modelling and analysis of infrastructure models and policies with actors to scrutinize security policies in the presence of insiders. We model insider attacks on airplanes in the Isabelle Insider framework. This application motivates the use of an extension of the framework with Kripke structures and the temporal logic CTL to enable reasoning on dynamic system states. Furthermore, we illustrate that Isabelle modelling and invariant reasoning reveal subtle security assumptions. We summarize by providing a methodology for the development of policies that satisfy stated properties.

Published
2020

3. An Introduction to Mechanized Reasoning

Author

Kerber, Manfred, Lange, Christoph, and Rowat, Colin

Subjects
Computer Science - Logic in Computer Science, 62P20, 91B26, 91B14, 68T15, 03B15, 03B10, F.4.1, I.2.3, J.4
Abstract

Mechanized reasoning uses computers to verify proofs and to help discover new theorems. Computer scientists have applied mechanized reasoning to economic problems but -- to date -- this work has not yet been properly presented in economics journals. We introduce mechanized reasoning to economists in three ways. First, we introduce mechanized reasoning in general, describing both the techniques and their successful applications. Second, we explain how mechanized reasoning has been applied to economic problems, concentrating on the two domains that have attracted the most attention: social choice theory and auction theory. Finally, we present a detailed example of mechanized reasoning in practice by means of a proof of Vickrey's familiar theorem on second-price auctions.

Published
2016
Full Text
View/download PDF

4. Budget Imbalance Criteria for Auctions: A Formalized Theorem

Author

Caminati, Marco B., Kerber, Manfred, and Rowat, Colin

Subjects
Quantitative Finance - Mathematical Finance, Computer Science - Computer Science and Game Theory, Computer Science - Logic in Computer Science, Quantitative Finance - Economics, 91B26 62P20
Abstract

We present an original theorem in auction theory: it specifies general conditions under which the sum of the payments of all bidders is necessarily not identically zero, and more generally not constant. Moreover, it explicitly supplies a construction for a finite minimal set of possible bids on which such a sum is not constant. In particular, this theorem applies to the important case of a second-price Vickrey auction, where it reduces to a basic result of which a novel proof is given. To enhance the confidence in this new theorem, it has been formalized in Isabelle/HOL: the main results and definitions of the formal proof are re- produced here in common mathematical language, and are accompanied by an informal discussion about the underlying ideas., Comment: 6th Podlasie Conference on Mathematics 2014, 11 pages

Published
2014

5. Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?

Author

Caminati, Marco B., Kerber, Manfred, Lange, Christoph, and Rowat, Colin

Subjects
Computer Science - Logic in Computer Science, 03E02, 03B35 (primary), 68W05 (Secondary), F.4.1, D.2.4, F.3.1
Abstract

When faced with the question of how to represent properties in a formal proof system any user has to make design decisions. We have proved three of the theorems from Maskin's 2004 survey article on Auction Theory using the Isabelle/HOL system, and we have produced verified code for combinatorial Vickrey auctions. A fundamental question in this was how to represent some basic concepts: since set theory is available inside Isabelle/HOL, when introducing new definitions there is often the issue of balancing the amount of set-theoretical objects and of objects expressed using entities which are more typical of higher order logic such as functions or lists. Likewise, a user has often to answer the question whether to use a constructive or a non-constructive definition. Such decisions have consequences for the proof development and the usability of the formalization. For instance, sets are usually closer to the representation that economists would use and recognize, while the other objects are closer to the extraction of computational content. In this paper we give examples of the advantages and disadvantages for these approaches and their relationships. In addition, we present the corresponding Isabelle library of definitions and theorems, most prominently those dealing with relations and quotients., Comment: Preprint of a paper accepted for the forthcoming CICM 2014 conference (cicm-conference.org/2014): S.M. Watt et al. (Eds.): CICM 2014, LNAI 8543, Springer International Publishing Switzerland 2014. 16 pages, 1 figure

Published
2014

6. Proving soundness of combinatorial Vickrey auctions and generating verified executable code

Author

Caminati, Marco B., Kerber, Manfred, Lange, Christoph, and Rowat, Colin

Subjects
Computer Science - Computer Science and Game Theory, Computer Science - Computational Engineering, Finance, and Science, Computer Science - Logic in Computer Science, 91-04, 68T15, 03B35, 91B26, 03B70, 03B15, J.4, D.2.4, F.4.1, I.2.4
Abstract

Using mechanised reasoning we prove that combinatorial Vickrey auctions are soundly specified in that they associate a unique outcome (allocation and transfers) to any valid input (bids). Having done so, we auto-generate verified executable code from the formally defined auction. This removes a source of error in implementing the auction design. We intend to use formal methods to verify new auction designs. Here, our contribution is to introduce and demonstrate the use of formal methods for auction verification in the familiar setting of a well-known auction.

Published
2013

7. A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory

Author

Lange, Christoph, Caminati, Marco B., Kerber, Manfred, Mossakowski, Till, Rowat, Colin, Wenzel, Makarius, and Windsteiger, Wolfgang

Subjects
Computer Science - Logic in Computer Science, Computer Science - Computer Science and Game Theory, Computer Science - Mathematical Software, 68T15, 03B35, 68T35, 91B26, 03B70, 03B10, 03B15, I.2.3, I.2.4, F.4.1, H.1.2, J.4
Abstract

Novel auction schemes are constantly being designed. Their design has significant consequences for the allocation of goods and the revenues generated. But how to tell whether a new design has the desired properties, such as efficiency, i.e. allocating goods to those bidders who value them most? We say: by formal, machine-checked proofs. We investigated the suitability of the Isabelle, Theorema, Mizar, and Hets/CASL/TPTP theorem provers for reproducing a key result of auction theory: Vickrey's 1961 theorem on the properties of second-price auctions. Based on our formalisation experience, taking an auction designer's perspective, we give recommendations on what system to use for formalising auctions, and outline further steps towards a complete auction theory toolbox., Comment: Conference on Intelligent Computer Mathematics, 8-12 July, Bath, UK. Published as number 7961 in Lecture Notes in Artificial Intelligence, Springer

Published
2013

8. The ForMaRE Project - Formal Mathematical Reasoning in Economics

Author

Lange, Christoph, Rowat, Colin, and Kerber, Manfred

Subjects
Computer Science - Computational Engineering, Finance, and Science, Computer Science - Logic in Computer Science, 91B26, 68T15, J.4, I.2.3, K.6.1
Abstract

The ForMaRE project applies formal mathematical reasoning to economics. We seek to increase confidence in economics' theoretical results, to aid in discovering new results, and to foster interest in formal methods, i.e. computer-aided reasoning, within economics. To formal methods, we seek to contribute user experience feedback from new audiences, as well as new challenge problems. In the first project year, we continued earlier game theory studies but then focused on auctions, where we are building a toolbox of formalisations, and have started to study matching and financial risk. In parallel to conducting research that connects economics and formal methods, we organise events and provide infrastructure to connect both communities, from fostering mutual awareness to targeted matchmaking. These efforts extend beyond economics, towards generally enabling domain experts to use mechanised reasoning., Comment: Conference on Intelligent Computer Mathematics, 8--12 July, Bath, UK. Published as number 7961 in Lecture Notes in Artificial Intelligence, Springer

Published
2013

9. Proofs, proofs, proofs, and proofs

Author

Kerber, Manfred

Subjects
Computer Science - Artificial Intelligence, Computer Science - Logic in Computer Science, Mathematics - History and Overview
Abstract

In logic there is a clear concept of what constitutes a proof and what not. A proof is essentially defined as a finite sequence of formulae which are either axioms or derived by proof rules from formulae earlier in the sequence. Sociologically, however, it is more difficult to say what should constitute a proof and what not. In this paper we will look at different forms of proofs and try to clarify the concept of proof in the wider meaning of the term. This has implications on how proofs should be represented formally., Comment: 10 pages, To appear in The 9th International Conference on Mathematical Knowledge Management: MKM 2010

Published
2010

10. A Proof and Some Representations

Author

Kerber, Manfred, Dillmann, Rüdiger, Series editor, Nakamura, Yoshihiko, Series editor, Schaal, Stefan, Series editor, Vernon, David, Series editor, Wyatt, Jeremy L., editor, Petters, Dean D., editor, and Hogg, David C., editor

Published
2014
Full Text
View/download PDF

11. Using Theorema in the Formalization of Theoretical Economics

Author

Kerber, Manfred, Rowat, Colin, Windsteiger, Wolfgang, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Goebel, Randy, editor, Siekmann, Jörg, editor, Wahlster, Wolfgang, editor, Davenport, James H., editor, Farmer, William M., editor, Urban, Josef, editor, and Rabe, Florian, editor

Published
2011
Full Text
View/download PDF

13. Heuristics for Resolution in Propositional Logic

Author

Kerber, Manfred, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Goebel, Randy, editor, Siekmann, Jörg, editor, Wahlster, Wolfgang, editor, Mertsching, Bärbel, editor, Hund, Marcus, editor, and Aziz, Zaheer, editor

Published
2009
Full Text
View/download PDF

15. A Dynamic Poincaré Principle

Author

Kerber, Manfred, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Borwein, Jonathan M., editor, and Farmer, William M., editor

Published
2006
Full Text
View/download PDF

16. A Tough Nut for Mathematical Knowledge Management

Author

Kerber, Manfred, Pollet, Martin, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, and Kohlhase, Michael, editor

Published
2006
Full Text
View/download PDF

18. Can a Higher-Order and a First-Order Theorem Prover Cooperate?

Author

Benzmüller, Christoph, Sorge, Volker, Jamnik, Mateja, Kerber, Manfred, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Baader, Franz, editor, and Voronkov, Andrei, editor

Published
2005
Full Text
View/download PDF

19. From MKRP to ΩMEGA

Author

Kerber, Manfred, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Hutter, Dieter, editor, and Stephan, Werner, editor

Published
2005
Full Text
View/download PDF

20. Why Is the Lucas-Penrose Argument Invalid?

Author

Kerber, Manfred, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, and Furbach, Ulrich, editor

Published
2005
Full Text
View/download PDF

21. Intuitive and Formal Representations: The Case of Matrices

Author

Pollet, Martin, Sorge, Volker, Kerber, Manfred, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Dough, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Asperti, Andrea, editor, Bancerek, Grzegorz, editor, and Trybulec, Andrzej, editor

Published
2004
Full Text
View/download PDF

22. High Classification Accuracy Does Not Imply Effective Genetic Search

Author

Kovacs, Tim, Kerber, Manfred, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Deb, Kalyanmoy, editor

Published
2004
Full Text
View/download PDF

23. Model-Guided Proof Planning

Author

Choi, Seungyeob, Kerber, Manfred, Gabbay, Dov M., editor, Barwise, Jon, editor, Magnani, Lorenzo, editor, Nersessian, Nancy J., editor, and Pizzi, Claudio, editor

Published
2002
Full Text
View/download PDF

24. LearnΩmatic: System Description

Author

Jamnik, Mateja, Kerber, Manfred, Pollet, Martin, Goos, G., editor, Hartmanis, J., editor, van Leeuwen, J., editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, and Voronkov, Andrei, editor

Published
2002
Full Text
View/download PDF

26. Experiments with an Agent-Oriented Reasoning System

Author

Benzmüller, Christoph, Kerber, Manfred, Jamnik, Mateja, Sorge, Volker, Goos, G., editor, Hartmanis, J., editor, van Leeuwen, J., editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Baader, Franz, editor, Brewka, Gerhard, editor, and Eiter, Thomas, editor

Published
2001
Full Text
View/download PDF

27. What Makes a Problem Hard for XCS?

Author

Kovacs, Tim, Kerber, Manfred, Goos, G., editor, Hartmanis, J., editor, van Leeuwen, J., editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Luca Lanzi, Pier, editor, Stolzmann, Wolfgang, editor, and Wilson, Stewart W., editor

Published
2001
Full Text
View/download PDF

28. Asymmetric majority pillage games

Author

Institute of Economic Research, Hitotsubashi University, Kerber, Manfred, Rowat, Colin, Yoshihara, Naoki, Institute of Economic Research, Hitotsubashi University, Kerber, Manfred, Rowat, Colin, and Yoshihara, Naoki

Abstract

We study pillage games (Jordan in J Econ Theory 131.1:26-44, 2006, “Pillage and property”), which model unstructured power contests. To enable empirical tests of pillage game theory, we relax a symmetry assumption that agents’ intrinsic contributions to a coalition’s power is identical. We characterise the core for all n. In the three-agent game: (i) only eight configurations are possible for the core, which contains at most six allocations; (ii) for each core configuration, the stable set is either unique or fails to exist; (iii) the linear power function creates a tension between a stable set’s existence and the interiority of its allocations, so that only special cases contain strictly interior allocations. Our analysis suggests that non-linear power functions may offer better empirical tests of pillage game theory.

Published
2022

31. On Knowledge, Strings, and Paradoxes

Author

Kerber, Manfred, Goos, G., editor, Hartmanis, J., editor, van Leeuwen, J., editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Dix, Jürgen, editor, del Cerro, Luís Fariñas, editor, and Furbach, Ulrich, editor

Published
1998
Full Text
View/download PDF

32. Mechanising partiality without re-implementation

Author

Kerber, Manfred, Kohlhase, Michael, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Goos, G., editor, Hartmanis, J., editor, van Leeuwen, J., editor, Brewka, Gerhard, editor, Habel, Christopher, editor, and Nebel, Bernhard, editor

Published
1997
Full Text
View/download PDF

33. Ωmega: Towards a mathematical assistant

Author

Benzmüller, Christoph, Cheikhrouhou, Lassaad, Fehrer, Detlef, Fiedler, Armin, Huang, Xiaorong, Kerber, Manfred, Kohlhase, Michael, Konrad, Karsten, Meier, Andreas, Melis, Erica, Schaarschmidt, Wolf, Siekmann, Jörg, Sorge, Volker, and McCune, William, editor

Published
1997
Full Text
View/download PDF

37. Adapting methods to novel tasks in proof planning

Author

Huang, Xiaorong, Kerber, Manfred, Kohlhase, Michael, Richts, Jörn, Goos, G., editor, Hartmanis, J., editor, van Leeuwen, J., editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Nebel, Bernhard, editor, and Dreschler-Fischer, Leonie, editor

Published
1994
Full Text
View/download PDF

38. KEIM: A toolkit for automated deduction

Author

Huang, Xiaorong, Kerber, Manfred, Kohlhase, Michael, Melis, Erica, Nesmith, Dan, Richts, Jörn, Siekmann, Jörg, Carbonell, J. G., editor, Siekmann, J., editor, Goos, G., editor, Hartmanis, J., editor, and Bundy, Alan, editor

Published
1994
Full Text
View/download PDF

39. Ω-MKRP: A proof development environment

Author

Huang, Xiaorong, Kerber, Manfred, Kohlhase, Michael, Melis, Erica, Nesmith, Dan, Richts, Jörn, Siekmann, Jörg, Carbonell, J. G., editor, Siekmann, J., editor, Goos, G., editor, Hartmanis, J., editor, and Bundy, Alan, editor

Published
1994
Full Text
View/download PDF

42. Applying the Isabelle insider framework to airplane security

Author

Kamm��ller, Florian and Kerber, Manfred

Subjects
Software Engineering (cs.SE), FOS: Computer and information sciences, Computer Science - Software Engineering, Computer Science - Logic in Computer Science, Logic in Computer Science (cs.LO)
Abstract

Avionics is one of the fields in which verification methods have been pioneered and brought about a new level of reliability to systems used in safety-critical environments. Tragedies, like the 2015 insider attack on a German airplane, in which all 150 people on board died, show that safety and security crucially depend not only on the well-functioning of systems but also on the way humans interact with the systems. Policies are a way to describe how humans should behave in their interactions with technical systems. Formal reasoning about such policies requires integrating the human factor into the verification process. In this paper, we report on our work on using logical modelling and analysis of infrastructure models and policies with actors to scrutinize security policies in the presence of insiders. An insider is a user of a system who behaves like an attacker abusing privileges thereby bypassing security controls. We model insider attacks on airplanes in the Isabelle Insider framework. This application motivates the use of an extension of the framework with Kripke structures and the temporal logic CTL to enable reasoning on dynamic system states. Furthermore, we illustrate that Isabelle modelling and invariant reasoning reveal subtle security assumptions. This results in a methodology for the development of policies that satisfy stated properties. To contrast our approach to model checking, we provide an additional comparative analysis.

Published
2021

Catalog

Books, media, physical & digital resources
See catalog results