혼 절
혼 절(Horn clause)은 수리 논리학 및 논리형 프로그래밍에서 논리형 프로그래밍, 형식 사양, 보편대수학 및 모형 이론에 사용하기 위한 유용한 속성을 제공하는 특정 규칙과 유사한 형식의 논리식이다. 혼 절의 이름은 1951년에 처음으로 그 중요성을 지적한 논리학자 앨프리드 혼의 이름을 따서 명명되었다.
정의
[편집]혼 절은 최대 하나의 긍정, 즉 부정되지 않은 리터럴을 포함하는 분리 절(리터럴의 분리)이다.
반대로, 최대 하나의 부정 리터럴을 갖는 리터럴의 분리를 이중 혼 절(dual-Horn clause)이라고 한다.
같이 보기
[편집]출처
[편집]- Burris, Stanley; Sankappanavar, H.P., 편집. (1981). 《A Course in Universal Algebra》. Springer-Verlag. ISBN 0-387-90578-2.
- Buss, Samuel R. (1998). 〈An Introduction to Proof Theory〉. Samuel R. Buss. 《Handbook of Proof Theory》. Studies in Logic and the Foundations of Mathematics 137. Elsevier B.V. 1–78쪽. doi:10.1016/S0049-237X(98)80016-5. ISBN 978-0-444-89840-1. ISSN 0049-237X.
- Chang, Chen Chung; Keisler, H. Jerome (1990) [1973]. 《Model Theory》. Studies in Logic and the Foundations of Mathematics 3판. Elsevier. ISBN 978-0-444-88054-3.
- Dowling, William F.; Gallier, Jean H. (1984). “Linear-time algorithms for testing the satisfiability of propositional Horn formulae”. 《Journal of Logic Programming》 1 (3): 267–284. doi:10.1016/0743-1066(84)90014-1.
- van Emden, M. H.; Kowalski, R. A. (1976). “The semantics of predicate logic as a programming language” (PDF). 《Journal of the ACM》 23 (4): 733–742. CiteSeerX 10.1.1.64.9246. doi:10.1145/321978.321991. S2CID 11048276.
- Horn, Alfred (1951). “On sentences which are true of direct unions of algebras”. 《Journal of Symbolic Logic》 16 (1): 14–21. doi:10.2307/2268661. JSTOR 2268661. S2CID 42534337.
- Lau, Kung-Kiu; Ornaghi, Mario (2004). 〈Specifying Compositional Units for Correct Program Development in Computational Logic〉. 《Program Development in Computational Logic》. Lecture Notes in Computer Science 3049. 1–29쪽. doi:10.1007/978-3-540-25951-0_1. ISBN 978-3-540-22152-4.
- Makowsky, J.A. (1987). “Why Horn Formulas Matter in Computer Science: Initial Structures and Generic Examples” (PDF). 《Journal of Computer and System Sciences》 34 (2–3): 266–292. doi:10.1016/0022-0000(87)90027-4.