Hennessy–Milner logic
કોમ્પ્યુટર વિજ્ઞાનમાં, હેનેસી-મિલનર તર્કશાસ્ત્ર (એચ. એમ. એલ.) એ એક ગતિશીલ તર્કશાસ્ત્ર છે જેનો ઉપયોગ લેબલ થયેલ સંક્રમણ પ્રણાલી (એલ. ટી. એસ.) ના ગુણધર્મોને સ્પષ્ટ કરવા માટે થાય છે, જે ઓટોમેટન જેવું માળખું છે. તે 1980 માં મેથ્યુ હેનેસી અને રોબિન મિલનર દ્વારા તેમના પેપર "ઓન ઓબ્ઝર્વેશન નોનડેટર્મિનિઝમ એન્ડ કોન્કરન્સી" (આઇસીએએલપી) માં રજૂ કરવામાં આવ્યું હતું. એચ. એમ. એલ. ના અન્ય પ્રકારમાં તર્કની અભિવ્યક્તિનો વિસ્તાર કરવા માટે પુનરાવર્તનનો ઉપયોગ થાય છે, અને તેને સામાન્ય રીતે 'પુનરાવર્તન સાથે હેનેસી-મિલનર તર્ક' તરીકે ઓળખવામાં આવે છે. મહત્તમ અને લઘુત્તમ નિશ્ચિત બિંદુઓના ઉપયોગ સાથે પુનરાવર્તન સક્ષમ કરવામાં આવે છે. વાક્યરચના A સૂત્રને એક્ટ માટે નીચેના BNF વ્યાકરણ દ્વારા વ્યાખ્યાયિત કરવામાં આવે છે, કેટલીક ક્રિયાઓના સમૂહઃ એટલે કે, એક સૂત્ર સતત સત્ય હોઈ શકે છે હંમેશા સાચું સતત ખોટું હંમેશા ખોટું સૂત્ર જોડાણ સૂત્ર બધા એક્ટ-ડેરિવેટિવ્ઝ માટે ડિસજંક્શન સૂત્ર, કેટલાક એક્ટ-ડેરિવેટિવ્ઝ માટે સૂત્ર હોવું આવશ્યક છે, ઔપચારિક સિમેન્ટિક્સ હોવું આવશ્યક છે. સંતોષકારક સંબંધ એલ. ટી. એસ. ની સ્થિતિઓને તેઓ જે સૂત્રોને સંતોષે છે તેની સાથે સંબંધિત કરે છે, અને તેને સૌથી નાના સંબંધ તરીકે વ્યાખ્યાયિત કરવામાં આવે છે, જેમ કે, તમામ સ્થિતિઓ અને સૂત્રો માટે, એવી કોઈ સ્થિતિ નથી કે જેના માટે, જો એવી સ્થિતિ અસ્તિત્વમાં હોય કે જે તે ધરાવે છે, તો પછી, જો, તો, તો, તો, પછી, જો, તો, અને પછી. મોડલ એમયુ-કેલ્ક્યુલસ પણ જુઓ, જે એચ. એમ. એલ. ને ફિક્સ્ડ પોઇન્ટ ઓપરેટર્સ ડાયનેમિક લોજિક સાથે વિસ્તરે છે, જે અનંત રીતે ઘણી પદ્ધતિઓ સાથે મલ્ટીમોડલ લોજિક છે. 1988. "હેનેસી-મિલનર લોજિક વિથ રિકર્શન એઝ એ સ્પષ્ટીકરણ લેંગ્વેજ, એન્ડ એ રિફાઇનમેન્ટ કેલ્ક્યુલસ બેઝ્ડ ઓન ઇટ". સમવર્તી પ્રણાલીઓના સ્પષ્ટીકરણ અને ચકાસણી પર BCS-FACS વર્કશોપની કાર્યવાહીમાં, ચાર્લ્સ રેટ્ટ્રે (એડ.). સ્પ્રિંગર-વેરલેગ, લંડન, યુકે, 294-330. સમવર્તી (કોમ્પ્યુટર વિજ્ઞાન) ઔપચારિક સ્પષ્ટીકરણ કોમ્પ્યુટર વિજ્ઞાનમાં મોડલ લોજિક લોજિક