Hennessy–Milner logic
ಗಣಕಯಂತ್ರ ವಿಜ್ಞಾನದಲ್ಲಿ, ಹೆನ್ನೆಸ್ಸಿ-ಮಿಲ್ನರ್ ತರ್ಕವು (ಎಚ್. ಎಂ. ಎಲ್.) ಒಂದು ಸ್ವಯಂಚಾಲಿತ ಯಂತ್ರಕ್ಕೆ ಹೋಲುವ ರಚನೆಯಾದ ಲೇಬಲ್ ಮಾಡಲಾದ ಪರಿವರ್ತನಾ ವ್ಯವಸ್ಥೆಯ (ಎಲ್. ಟಿ. ಎಸ್.) ಗುಣಲಕ್ಷಣಗಳನ್ನು ನಿರ್ದಿಷ್ಟಪಡಿಸಲು ಬಳಸುವ ಕ್ರಿಯಾತ್ಮಕ ತರ್ಕವಾಗಿದೆ. ಇದನ್ನು 1980 ರಲ್ಲಿ ಮ್ಯಾಥ್ಯೂ ಹೆನ್ನೆಸ್ಸಿ ಮತ್ತು ರಾಬಿನ್ ಮಿಲ್ನರ್ ಅವರು ತಮ್ಮ ಪ್ರಬಂಧ "ಆನ್ ಅಬ್ಸರ್ಬಿಂಗ್ ನಾನ್ ಡಿಟರ್ಮಿನಿಸಂ ಅಂಡ್ ಕಾನ್ಕರೆನ್ಸಿ" (ಐಸಿಎಎಲ್ಪಿ) ಯಲ್ಲಿ ಪರಿಚಯಿಸಿದರು. ಎಚ್ಎಂಎಲ್ನ ಮತ್ತೊಂದು ರೂಪಾಂತರವು ತರ್ಕದ ಅಭಿವ್ಯಕ್ತಿಯನ್ನು ವಿಸ್ತರಿಸಲು ಪುನರಾವರ್ತನೆಯ ಬಳಕೆಯನ್ನು ಒಳಗೊಂಡಿರುತ್ತದೆ ಮತ್ತು ಇದನ್ನು ಸಾಮಾನ್ಯವಾಗಿ 'ಪುನರಾವರ್ತನೆಯೊಂದಿಗೆ ಹೆನ್ನೆಸ್ಸಿ-ಮಿಲ್ನರ್ ಲಾಜಿಕ್' ಎಂದು ಕರೆಯಲಾಗುತ್ತದೆ. ಗರಿಷ್ಠ ಮತ್ತು ಕನಿಷ್ಠ ಸ್ಥಿರ ಅಂಕಗಳ ಬಳಕೆಯೊಂದಿಗೆ ಪುನರಾವರ್ತನೆಯನ್ನು ಸಕ್ರಿಯಗೊಳಿಸಲಾಗಿದೆ. ವಾಕ್ಯರಚನೆಯ ಸೂತ್ರವನ್ನು ಕಾಯಿದೆಯ ಕೆಲವು ಕ್ರಿಯೆಗಳ ಗುಂಪಿಗಾಗಿ ಈ ಕೆಳಗಿನ ಬಿ. ಎನ್. ಎಫ್ ವ್ಯಾಕರಣದಿಂದ ವ್ಯಾಖ್ಯಾನಿಸಲಾಗಿದೆಃ ಅಂದರೆ, ಒಂದು ಸೂತ್ರವು ಸ್ಥಿರವಾದ ಸತ್ಯವಾಗಿರಬಹುದು ಯಾವಾಗಲೂ ಸತ್ಯ ಸ್ಥಿರವಾದ ಸುಳ್ಳು ಯಾವಾಗಲೂ ಸುಳ್ಳು ಸೂತ್ರ ಸಂಯೋಜನೆಯ ಸೂತ್ರವು ಎಲ್ಲಾ ಕಾಯಿದೆಯ-ವ್ಯುತ್ಪತ್ತಿಗಳಿಗೆ ಸೂತ್ರವನ್ನು ಹೊಂದಿರಬೇಕು, ಕೆಲವು ಕಾಯಿದೆಯ-ವ್ಯುತ್ಪತ್ತಿಗೆ ಸೂತ್ರವನ್ನು ಹೊಂದಿರಬೇಕು, ಔಪಚಾರಿಕ ಶಬ್ದಾರ್ಥವನ್ನು ಹೊಂದಿರಬೇಕು. ತೃಪ್ತಿಯ ಸಂಬಂಧವು ಎಲ್ಟಿಎಸ್ನ ಸ್ಥಿತಿಗಳನ್ನು ಅವು ತೃಪ್ತಿಪಡಿಸುವ ಸೂತ್ರಗಳಿಗೆ ಸಂಬಂಧಿಸುತ್ತದೆ, ಮತ್ತು ಎಲ್ಲಾ ಸ್ಥಿತಿಗಳು ಮತ್ತು ಸೂತ್ರಗಳಿಗೆ, ಅಂತಹ ಸ್ಥಿತಿ ಅಸ್ತಿತ್ವದಲ್ಲಿದ್ದರೆ ಯಾವುದೇ ಸ್ಥಿತಿ ಇಲ್ಲ ಮತ್ತು, ನಂತರ, ಅದು ಹೊಂದಿರುವ ಎಲ್ಲದಕ್ಕೂ, ಆಗ, ಆಗ, ಆಗ, ಆಗ, ಆಗ, ಆಗ, ಆಗ, ಆಗ, ಆಗ, ಆಗ, ಆಗ. ಸ್ಥಿರ ಬಿಂದು ಆಪರೇಟರ್ಗಳಾದ ಡೈನಾಮಿಕ್ ಲಾಜಿಕ್ ನೊಂದಿಗೆ ಎಚ್. ಎಂ. ಎಲ್ ಅನ್ನು ವಿಸ್ತರಿಸುವ ಮಾಡಲ್ ಮ್ಯೂ-ಕ್ಯಾಲ್ಕುಲಸ್ ಅನ್ನು ಸಹ ನೋಡಿ, ಇದು ಅನಂತವಾದ ಅನೇಕ ವಿಧಾನಗಳನ್ನು ಹೊಂದಿರುವ ಬಹುವಿಧದ ತರ್ಕವಾಗಿದೆ. 1988 ರಲ್ಲಿ. "ಹೆನ್ನೆಸ್ಸಿ-ಮಿಲ್ನರ್ ಲಾಜಿಕ್ ವಿತ್ ರಿಕರ್ಶನ್ ಆಸ್ ಎ ಸ್ಪೆಸಿಫಿಕೇಷನ್ ಲಾಂಗ್ವೇಜ್, ಅಂಡ್ ಎ ರಿಫೈನ್ಮೆಂಟ್ ಕ್ಯಾಲ್ಕುಲಸ್ ಬೇಸ್ಡ್ ಇಟ್". ಪ್ರೊಸೀಡಿಂಗ್ಸ್ ಆಫ್ ದಿ ಬಿಸಿಎಸ್-ಎಫ್ಎಸಿಎಸ್ ವರ್ಕ್ಶಾಪ್ ಆನ್ ಸ್ಪೆಸಿಫಿಕೇಷನ್ ಅಂಡ್ ವೆರಿಫಿಕೇಷನ್ ಆಫ್ ಕಾಂಕರೆಂಟ್ ಸಿಸ್ಟಮ್ಸ್ನಲ್ಲಿ, ಚಾರ್ಲ್ಸ್ ರಾಟ್ರೇ (ಎಡ್.). ಸ್ಪ್ರಿಂಗರ್-ವೆರ್ಲಾಗ್, ಲಂಡನ್, ಯುಕೆ, 294-330. ಸಮವರ್ತಿ (ಗಣಕಯಂತ್ರ ವಿಜ್ಞಾನ) ಔಪಚಾರಿಕ ವಿವರಣೆ ಗಣಕಯಂತ್ರ ವಿಜ್ಞಾನದಲ್ಲಿ ಮಾದರಿ ತರ್ಕ ತರ್ಕ