Sign In

Functional Stable Model Semantics and Answer Set Programming Modulo Theories

μž‘μ„±μž
  • Haebom
μΉ΄ν…Œκ³ λ¦¬
Empty

μ €μž

Michael Bartholomew, Joohyung Lee

πŸ’‘ κ°œμš”

λ³Έ 논문은 Answer Set Programming(ASP)μ—μ„œ 'λ‚΄μž¬μ  ν•¨μˆ˜'λ₯Ό ν†΅ν•©ν•˜λŠ” μƒˆλ‘œμš΄ μ ‘κ·Ό 방식을 μ œμ•ˆν•©λ‹ˆλ‹€. κΈ°μ‘΄ ASP의 ν•œκ³„λ₯Ό κ·Ήλ³΅ν•˜κΈ° μœ„ν•΄ μ œμ•ˆλœ 'κΈ°λŠ₯적 μ•ˆμ • λͺ¨λΈ 의미둠(functional stable model semantics)'은 ASP와 Satisfiability Modulo Theories(SMT)λ₯Ό ν†΅ν•©ν•œ ASPMT ν”„λ ˆμž„μ›Œν¬μ—μ„œ μ€‘μš”ν•œ 역할을 ν•©λ‹ˆλ‹€. 이λ₯Ό 톡해 κΈ°μ‘΄ ASPMT 톡합 방식듀이 νŠΉμ • ν•¨μˆ˜μ˜ μ œν•œμ μΈ μ—­ν• λ§Œμ„ μˆ˜ν–‰ν•˜λŠ” νŠΉμˆ˜ν•œ 경우둜 μ„€λͺ…될 수 μžˆμŒμ„ 보이고, "νƒ€μ΄νŠΈν•œ(tight)" ASPMT ν”„λ‘œκ·Έλž¨μ„ SMT μΈμŠ€ν„΄μŠ€λ‘œ λ³€ν™˜ν•  수 μžˆμŒμ„ λ³΄μ—¬μ€λ‹ˆλ‹€.

πŸ”‘ μ‹œμ‚¬μ  및 ν•œκ³„

β€’
λ‚΄μž¬μ  ν•¨μˆ˜λ₯Ό ASP에 ν†΅ν•©ν•¨μœΌλ‘œμ¨ 문제 ν•΄κ²° λŠ₯λ ₯을 ν™•μž₯ν•  수 μžˆμŠ΅λ‹ˆλ‹€.
β€’
ASPMT ν”„λ ˆμž„μ›Œν¬λŠ” ASP와 SMT의 강점을 κ²°ν•©ν•˜μ—¬ 보닀 κ°•λ ₯ν•œ μΆ”λ‘  κΈ°λŠ₯을 μ œκ³΅ν•©λ‹ˆλ‹€.
β€’
"νƒ€μ΄νŠΈν•œ" ASPMT ν”„λ‘œκ·Έλž¨μ˜ SMT λ³€ν™˜μ€ 효율적인 해결을 μœ„ν•œ μƒˆλ‘œμš΄ 길을 μ—΄μ–΄μ€λ‹ˆλ‹€.
β€’
μ œμ•ˆλœ λ°©λ²•λ‘ μ˜ 일반적인 ASPMT ν”„λ‘œκ·Έλž¨μœΌλ‘œμ˜ ν™•μž₯ κ°€λŠ₯μ„± 및 μ‹€μ œ μ‘μš©μ—μ„œμ˜ μ„±λŠ₯ 검증이 ν–₯ν›„ κ³Όμ œμž…λ‹ˆλ‹€.
πŸ‘