Semantic minimization of 3-valued propositional formulae

T. Reps1, A. Loginov1, M. Sagiv2
1Comp. Sci. Department, University of Wisconsin, Madison, WI, USA
2School of Comp. Sci, Tel-Aviv University, Tel-Aviv, Israel

Tóm tắt

This paper presents an algorithm for a non-standard logic-minimization problem that arises in 3-valued propositional logic. The problem is motivated by the potential for obtaining better answers in applications that use 3-valued logic. An answer of 0 or 1 provides precise (definite) information; an answer of 1/2 provides imprecise (indefinite) information. By replacing a formula /spl phi/ with a "better" formula /spl psi/, we may improve the precision of the answers obtained. In this paper we give an algorithm that always produces a formula that is "best" (in a certain well-defined sense).

Từ khóa

#Logic #Hardware #Data analysis #Information analysis #Software systems #Uncertainty #Contracts #Terminology #Minimization methods

Tài liệu tham khảo

10.1145/514188.514190 10.1007/978-1-4613-1385-4 10.2307/2308219 10.1007/BF01383966 10.1145/292540.292552 10.2307/2024549 minato, 1992, Fast generation of irredundant sum-of-products forms from binary decision diagrams, Proc 6th Workshop on Synth and Syst Integr of Mixed Technol, 64 10.1109/DAC.1990.114828 kleene, 1987, Introduction to Metamathematics lev-ami, 2000, TVLA: A system for implementing static analyses, Proc Static Analysis Symp, 280, 10.1007/978-3-540-45099-3_15 10.1111/j.1467-8640.1988.tb00280.x jain, 1997, Formal Verification by Symbolic Trajectory Evaluation sasao, 0, Ternary decision diagrams and their applications, 269 10.1177/0010414001034001001 10.1007/s002360050128 blamey, 1980, Partial Valued Logic 10.1007/978-94-017-0458-8_5 coudert, 1993, Implicit prime cover computation: An overview, Proc 6th Workshop on Synth and Syst Integr of Mixed Technol chou, 1999, The mathematical foundation of symbolic trajectory evaluation, Comput Aided Verif, 10.1007/3-540-48683-6_19 10.1109/TC.1986.1676819 10.1109/DAC.1990.114826 bodik, 1998, Complete removal of redundant computations, ACM SIGPLAN Conf Prog Lang Design and Implement, 1 10.1007/978-1-4615-3154-8_2 10.1016/0167-9260(94)00007-7