{"@context":["https://w3id.org/fdo/context/v1",{"schema":"https://schema.org/","prov":"http://www.w3.org/ns/prov#","fdo":"https://w3id.org/fdo/vocabulary/"}],"@id":"https://fdo.portal.mardi4nfdi.de/fdo/Q580955","@type":"DigitalObject","kernel":{"@id":"https://fdo.portal.mardi4nfdi.de/fdo/Q580955","digitalObjectType":"https://schema.org/ScholarlyArticle","primaryIdentifier":"mardi:Q580955","kernelVersion":"v1","immutable":true,"modified":"2026-01-06T14:24:27Z"},"profile":{"@context":"https://schema.org","@type":"ScholarlyArticle","@id":"https://portal.mardi4nfdi.de/entity/Q580955","name":"Total correctness in nonstandard logics of programs","headline":"Total correctness in nonstandard logics of programs","description":"scientific article; zbMATH DE number 4018356","url":"https://portal.mardi4nfdi.de/entity/Q580955","datePublished":"1987-00-00","author":[{"@id":"https://portal.mardi4nfdi.de/entity/Q514567"}],"publisher":[{"@id":"https://portal.mardi4nfdi.de/entity/Q123643"}],"identifier":{"@type":"PropertyValue","propertyID":"doi","value":"10.1016/0304-3975(87)90118-6","url":"https://doi.org/10.1016/0304-3975(87)90118-6"},"sameAs":["https://doi.org/10.1016/0304-3975(87)90118-6"],"comment":"We show that termination is a first-order notion if approached via nonstandard logics of programs (NLP). We give explicit first-order characterizations of the program-verifying power of the well-known Mann- Cooper method for proving total correctness assertions (tca's). Similar characterization is given to the intermittent assertions method (w.r.t. tca's). A comparison of the tca-proving powers of distinguished methods (or logics of programs) is also attempted. We also show that NLP provided new methods which are strictly stronger than the Mann-Cooper method. In the end we turn to partial correctness issues related to the main body of the paper.","citation":[{"@id":"https://portal.mardi4nfdi.de/entity/Q3309036"},{"@id":"https://portal.mardi4nfdi.de/entity/Q1159461"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3939224"},{"@id":"https://portal.mardi4nfdi.de/entity/Q4054648"},{"@id":"https://portal.mardi4nfdi.de/entity/Q5184385"},{"@id":"https://portal.mardi4nfdi.de/entity/Q5679729"},{"@id":"https://portal.mardi4nfdi.de/entity/Q1162355"},{"@id":"https://portal.mardi4nfdi.de/entity/Q760793"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3960106"},{"@id":"https://portal.mardi4nfdi.de/entity/Q1822934"},{"@id":"https://portal.mardi4nfdi.de/entity/Q4726228"},{"@id":"https://portal.mardi4nfdi.de/entity/Q1087866"},{"@id":"https://portal.mardi4nfdi.de/entity/Q4095834"},{"@id":"https://portal.mardi4nfdi.de/entity/Q4124327"},{"@id":"https://portal.mardi4nfdi.de/entity/Q4190096"},{"@id":"https://portal.mardi4nfdi.de/entity/Q4144164"},{"@id":"https://portal.mardi4nfdi.de/entity/Q4124795"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3956390"},{"@id":"https://portal.mardi4nfdi.de/entity/Q1077159"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3744163"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3896482"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3345770"},{"@id":"https://portal.mardi4nfdi.de/entity/Q801661"},{"@id":"https://portal.mardi4nfdi.de/entity/Q910396"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3698302"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3956920"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3678651"}]},"provenance":{"prov:generatedAtTime":"2026-01-06T14:24:27Z","prov:wasAttributedTo":"MaRDI Knowledge Graph"}}