Formalization of Cost and Utility in Microeconomics

Asad Ahmed, Osman Hasan, Falah Awwad and Nabil Bastaki
Additional contact information
Asad Ahmed: School of Electrical Engineering and Computer Science, National University of Sciences and Technology (NUST), Islamabad H-12, Pakistan
Osman Hasan: School of Electrical Engineering and Computer Science, National University of Sciences and Technology (NUST), Islamabad H-12, Pakistan
Falah Awwad: College of Engineering, United Arab Emirates University, Al-Ain 15551, UAE
Nabil Bastaki: College of Engineering, United Arab Emirates University, Al-Ain 15551, UAE

Energies, 2020, vol. 13, issue 3, 1-19

Abstract: Cost and utility modeling of economics agents based on the differential theory is fundamental to the analysis of the microeconomics models. In particular, the first and second-order derivative tests are used to specify the desired properties of the cost and utility models. Traditionally, paper-and-pencil proof methods and computer-based tools are used to investigate the mathematical properties of these models. However, these techniques do not provide an accurate analysis due to their inability to exhaustively specify and verify the mathematical properties of the cost and utility models. Additionally, these techniques cannot accurately model and analyze pure continuous behaviors of the economic agents due to the utilization of computer arithmetic. On the other hand, an accurate analysis is direly needed in many safety and cost-critical microeconomics applications, such as agriculture and smart grids. To overcome the issues pertaining to the above-mentioned techniques, in this paper, we propose a theorem proving based methodology to formally analyze and specify the mathematical properties of functions used in microeconomics modeling. The proposed methodology is primarily based on a formalization of the derivative tests and root analysis of the polynomial functions, within the sound core of the HOL-Light theorem prover. We also provide a formalization of the first-order condition, which is used to analyze the maximum of the profit function in a higher-order-logic theorem prover. We then present the formal analysis of the utility, cost and first-order condition based on the polynomial functions. To illustrate the usefulness of proposed formalization, the proposed formalization is used to formally analyze and verify the quadratic cost and utility functions, which have been used in an optimal power flow problem and demand response (DR) program, respectively.

Keywords: microeconomics; electricity market; cost function; utility function; HOL-light (search for similar items in EconPapers)
JEL-codes: Q Q0 Q4 Q40 Q41 Q42 Q43 Q47 Q48 Q49 (search for similar items in EconPapers)
Date: 2020
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/1996-1073/13/3/712/pdf (application/pdf)
https://www.mdpi.com/1996-1073/13/3/712/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jeners:v:13:y:2020:i:3:p:712-:d:317418

Access Statistics for this article

Energies is currently edited by Ms. Agatha Cao

More articles in Energies from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().