Proof compression
ಗಣಿತದ ತರ್ಕದ ಒಂದು ಕ್ಷೇತ್ರವಾದ ಪ್ರೂಫ್ ಥಿಯರಿಯಲ್ಲಿ, ಪ್ರೂಫ್ ಕಂಪ್ರೆಷನ್ ಎಂಬುದು ಕ್ರಮಾವಳಿಗಳ ಮೂಲಕ ಔಪಚಾರಿಕ ಪುರಾವೆಗಳನ್ನು ಸಂಕುಚಿತಗೊಳಿಸುವ ಸಮಸ್ಯೆಯಾಗಿದೆ. ಅಭಿವೃದ್ಧಿಪಡಿಸಿದ ಕ್ರಮಾವಳಿಗಳನ್ನು ಎಸ್. ಎ. ಟಿ. ಪರಿಹಾರಗಳು, ಎಸ್. ಎಂ. ಟಿ.-ಪರಿಹಾರಗಳು, ಪ್ರಥಮ-ಕ್ರಮಾಂಕದ ಪ್ರಮೇಯ ನಿರೂಪಣೆಗಳು ಮತ್ತು ಪುರಾವೆ ಸಹಾಯಕರಂತಹ ಸ್ವಯಂಚಾಲಿತ ಪ್ರಮೇಯವನ್ನು ಸಾಬೀತುಪಡಿಸುವ ಸಾಧನಗಳಿಂದ ಉತ್ಪತ್ತಿಯಾಗುವ ಪುರಾವೆಗಳನ್ನು ಸುಧಾರಿಸಲು ಬಳಸಬಹುದು. ಸಮಸ್ಯೆಯ ಪ್ರಾತಿನಿಧ್ಯ ಪ್ರತಿಪಾದನೆಯ ತರ್ಕದಲ್ಲಿ, ಸಿ ಷರತ್ತುಗಳ ಗುಂಪಿನಿಂದ ಒಂದು ಷರತ್ತಿನ ರೆಸಲ್ಯೂಶನ್ ಪುರಾವೆಯು ನಿರ್ದೇಶಿತ ಅಸೈಕ್ಲಿಕ್ ಗ್ರಾಫ್ (ಡಿ. ಎ. ಜಿ) ಆಗಿದೆಃ ಇನ್ಪುಟ್ ನೋಡ್ಗಳು ಸ್ವಯಂಸಿದ್ಧ ತೀರ್ಮಾನಗಳಾಗಿವೆ (ಆವರಣವಿಲ್ಲದೆ) ಅವುಗಳ ತೀರ್ಮಾನಗಳು ಸಿ ಯ ಅಂಶಗಳಾಗಿವೆ, ರೆಸಲ್ಯೂಶನ್ ನೋಡ್ಗಳು ರೆಸಲ್ಯೂಶನ್ ತೀರ್ಮಾನಗಳಾಗಿವೆ, ಮತ್ತು ಪುರಾವೆಯು ತೀರ್ಮಾನದೊಂದಿಗೆ ನೋಡ್ ಅನ್ನು ಹೊಂದಿದೆ. ಒಂದು ಪ್ರಮೇಯವು ಅದರ ತೀರ್ಮಾನವಾಗಿದ್ದರೆ ಮಾತ್ರ ಡಿ. ಎ. ಜಿ. ಯು ನೋಡ್ನಿಂದ ನೋಡ್ಗೆ ಒಂದು ಅಂಚನ್ನು ಹೊಂದಿರುತ್ತದೆ. ಈ ಸಂದರ್ಭದಲ್ಲಿ, ಇದು ಅವರ ಮಗುವಾಗಿದೆ ಮತ್ತು ಅವರ ಪೋಷಕರಾಗಿದ್ದಾರೆ. ಮಕ್ಕಳಿಲ್ಲದ ನೋಡ್ ಒಂದು ಮೂಲವಾಗಿದೆ. ಪ್ರೂಫ್ ಕಂಪ್ರೆಷನ್ ಅಲ್ಗಾರಿದಮ್ ಕಡಿಮೆ ನೋಡ್ಗಳೊಂದಿಗೆ ಹೊಸ ಡಿಎಜಿಯನ್ನು ರಚಿಸಲು ಪ್ರಯತ್ನಿಸುತ್ತದೆ, ಅದು ಮಾನ್ಯವಾದ ಪುರಾವೆಯನ್ನು ಪ್ರತಿನಿಧಿಸುತ್ತದೆ ಅಥವಾ ಕೆಲವು ಸಂದರ್ಭಗಳಲ್ಲಿ, ಅದರ ಉಪವಿಭಾಗದ ಮಾನ್ಯ ಪುರಾವೆಯಾಗಿದೆ. ಒಂದು ಸರಳ ಉದಾಹರಣೆ ಷರತ್ತುಗಳ ಗುಂಪಿನಿಂದ ಷರತ್ತಿಗೆ ರೆಸಲ್ಯೂಶನ್ ಪುರಾವೆಯನ್ನು ತೆಗೆದುಕೊಳ್ಳೋಣ ಇಲ್ಲಿ ನಾವು ನೋಡಬಹುದುಃ ಮತ್ತು ಇನ್ಪುಟ್ ನೋಡ್ಗಳಾಗಿವೆ. ನೋಡ್ ಒಂದು ಪಿವೋಟ್ ಅನ್ನು ಹೊಂದಿದೆ, ಲೆಫ್ಟ್ ರೆಸಲ್ಯೂಶನ್ ರೈಟ್ ರೆಸಲ್ಯೂಶನ್ ಅಕ್ಷರಶಃ ತೀರ್ಮಾನವು ಷರತ್ತು ಆವರಣಗಳು ನೋಡ್ಗಳ ತೀರ್ಮಾನವಾಗಿದೆ ಮತ್ತು (ಅದರ ಪೋಷಕರು) ಡಿಎಜಿ ಮಕ್ಕಳ ಪೋಷಕರು ಮತ್ತು ಪುರಾವೆಯ ಮೂಲವಾಗಿದೆ ಎ (ರೆಸಲ್ಯೂಶನ್) ಸಿ ಯ ನಿರಾಕರಣೆಯು ಸಿ ಯಿಂದ ರೆಸಲ್ಯೂಶನ್ ಪುರಾವೆಯಾಗಿದೆ. ಇದು ಸಾಮಾನ್ಯವಾದ ನೋಡ್ ಆಗಿದೆ, ಷರತ್ತು ಅಥವಾ ಷರತ್ತು ಎಂದರೆ ತೀರ್ಮಾನದ ಷರತ್ತು, ಮತ್ತು (ಉಪ) ಪುರಾವೆ ಎಂದರೆ (ಉಪ) ಪುರಾವೆ ಅದರ ಏಕೈಕ ಮೂಲವಾಗಿದೆ. ಕೆಲವು ಕೃತಿಗಳಲ್ಲಿ ರೆಸಲ್ಯೂಶನ್ ತೀರ್ಮಾನಗಳ ಬೀಜಗಣಿತದ ಪ್ರಾತಿನಿಧ್ಯವನ್ನು ಕಾಣಬಹುದು. ಪಿವೋಟ್ನ ಮತ್ತು ಅದರೊಂದಿಗಿನ ರಿಸಾಲ್ವೆಂಟ್ ಅನ್ನು ಹೀಗೆ ಸೂಚಿಸಬಹುದು. ಕೇಂದ್ರಬಿಂದುವನ್ನು ಅನನ್ಯವಾಗಿ ವ್ಯಾಖ್ಯಾನಿಸಿದಾಗ ಅಥವಾ ಅಪ್ರಸ್ತುತವಾದಾಗ, ನಾವು ಅದನ್ನು ಬಿಟ್ಟುಬಿಡುತ್ತೇವೆ ಮತ್ತು ಸರಳವಾಗಿ ಬರೆಯುತ್ತೇವೆ. ಈ ರೀತಿಯಾಗಿ, ಷರತ್ತುಗಳ ಗುಂಪನ್ನು ಕಮ್ಯುಟೇಟಿವ್ ಆಪರೇಟರ್ನೊಂದಿಗೆ ಬೀಜಗಣಿತವಾಗಿ ನೋಡಬಹುದು; ಮತ್ತು ಅನುಗುಣವಾದ ಪದ ಬೀಜಗಣಿತದಲ್ಲಿನ ಪದಗಳು ಸಾಮಾನ್ಯ ಗ್ರಾಫ್ ಸಂಕೇತಕ್ಕಿಂತ ರೆಸಲ್ಯೂಶನ್ ಪುರಾವೆಗಳನ್ನು ವಿವರಿಸಲು ಹೆಚ್ಚು ಸಾಂದ್ರವಾದ ಮತ್ತು ಹೆಚ್ಚು ಅನುಕೂಲಕರವಾದ ಸಂಕೇತ ಶೈಲಿಯಲ್ಲಿ ರೆಸಲ್ಯೂಶನ್ ಪುರಾವೆಗಳನ್ನು ಸೂಚಿಸುತ್ತವೆ. ನಮ್ಮ ಕೊನೆಯ ಉದಾಹರಣೆಯಲ್ಲಿ ಡಿ. ಎ. ಜಿ. ಯ ಸಂಕೇತವು ಸರಳವಾಗಿ ನಾವು ಗುರುತಿಸಬಹುದು. ಸಂಕೋಚನ ಕ್ರಮಾವಳಿಗಳು ಅನುಕ್ರಮ ಕಲನಶಾಸ್ತ್ರದ ಪುರಾವೆಗಳ ಸಂಕೋಚನಕ್ಕಾಗಿ ಕ್ರಮಾವಳಿಗಳು ಕಟ್ ಪರಿಚಯ ಮತ್ತು ಕಟ್ ಎಲಿಮಿನೇಷನ್ ಅನ್ನು ಒಳಗೊಂಡಿವೆ. ಪ್ರೊಪೊಸಿಷನಲ್ ರೆಸಲ್ಯೂಶನ್ ಪ್ರೂಫ್ಗಳ ಸಂಕೋಚನದ ಕ್ರಮಾವಳಿಗಳಲ್ಲಿ ರೀಸೈಕಲ್ ಯುನಿಟ್ಗಳು, ರೀಸೈಕಲ್ ಪಿವೋಟ್ಗಳು, ರೀಸೈಕಲ್ ಪಿವೋಟ್ಗಳು, ಇಂಟರ್ಸೆಕ್ಷನ್, ಲೋವರ್ ಯುನಿಟ್ಗಳು, ಲೋವರ್ ಯುನಿವೆಲೆಂಟ್ಗಳು, ಸ್ಪ್ಲಿಟ್, ರಿಡ್ಯೂಸ್ ಮತ್ತು ರಿಕನ್ಸ್ಟ್ರಕ್ಟ್ ಮತ್ತು ಸಬ್ಸಂಪ್ಶನ್ ಸೇರಿವೆ. ಟಿಪ್ಪಣಿಗಳ ಪುರಾವೆ ಸಿದ್ಧಾಂತ