A connection method for a defeasible extension of ALCH

A connection method for a defeasible extension of ALCH | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Research Article A connection method for a defeasible extension of ALCH Renan Fernandes, Fred Freitas, Ivan Varzinczak, Pedro P. M. Farias This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-4818202/v1 This work is licensed under a CC BY 4.0 License Status: Posted Version 1 posted You are reading this latest preprint version Abstract The development of proof methods for defeasible description logics (DLs), following those for classical DLs, is mainly based on semantic tableaux.However, the literature offers equally viable alternatives for automated theorem proving, such as the connection method.It consists of a goal-oriented direct proof search method that searches for connections (complementary pairs of literals) in a set of literals organized in clauses called a matrix.This paper presents a connection method for an exception-tolerant family of DLs.In that regard, (i) we use the language of ALCH extended with a typicality operator on concepts and another one on roles; (ii) we revisit the definition of a matrix representation of a knowledge base and establish the conditions for a given axiom to be provable from this matrix with a new normal form (Bi-Typicality Normal Form); (iii) we show how to handle term unification and define a suitable blocking condition in the presence of typicality operators; and (iv) we establish correctness, completeness, and termination of our algorithm. Connection method Description logic Defeasible logics Web Semantics Full Text Additional Declarations No competing interests reported. Cite Share Download PDF Status: Posted Version 1 posted You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {"props":{"pageProps":{"initialData":{"identity":"rs-4818202","acceptedTermsAndConditions":true,"allowDirectSubmit":true,"archivedVersions":[],"articleType":"Research Article","associatedPublications":[],"authors":[{"id":343322951,"identity":"693b98db-7388-4f42-9dfa-54f9ae95cce3","order_by":0,"name":"Renan Fernandes","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAAAu0lEQVRIiWNgGAWjYDACdsbnHz4wSABZjA+AxAEitDAzmzHOAGthNiBeCzMPhEWkFvNmZrbHNjUWeQwSyWwPPjDcySeoReYwM7txzjGJYqAWdsMZDM8sGwhpkWDmPyCd2yCR2CCRf0yah+GwAUFbJJiZGaQtwVqS2aT/EKmFTZoRpoWBSC3Mhj3HJBLbeB6zG/YYPCNCC3sz44MfNXWJ/ezAEPtRcYewFjhgAyMSNMB0jYJRMApGwSjAAgDEWi8p9VJV/AAAAABJRU5ErkJggg==","orcid":"","institution":"Federal University of Pernambuco","correspondingAuthor":true,"prefix":"","firstName":"Renan","middleName":"","lastName":"Fernandes","suffix":""},{"id":343322952,"identity":"5f88134c-1ddc-4a54-84d3-d31373444af7","order_by":1,"name":"Fred Freitas","email":"","orcid":"","institution":"Federal University of Pernambuco","correspondingAuthor":false,"prefix":"","firstName":"Fred","middleName":"","lastName":"Freitas","suffix":""},{"id":343322953,"identity":"00ba8155-77e3-47e1-9b45-fa1912f1ab15","order_by":2,"name":"Ivan Varzinczak","email":"","orcid":"","institution":"Paris 8 University","correspondingAuthor":false,"prefix":"","firstName":"Ivan","middleName":"","lastName":"Varzinczak","suffix":""},{"id":343322955,"identity":"991c133b-222f-4e0f-961c-c292419da510","order_by":3,"name":"Pedro P. M. Farias","email":"","orcid":"","institution":"Public Services Regulation Agency-CE","correspondingAuthor":false,"prefix":"","firstName":"Pedro","middleName":"P. M.","lastName":"Farias","suffix":""}],"badges":[],"createdAt":"2024-07-28 22:41:47","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-4818202/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-4818202/v1","draftVersion":[],"editorialEvents":[],"editorialNote":"","failedWorkflow":false,"files":[{"id":104026595,"identity":"b99ed524-43f3-4ab9-9a82-bb0d754cbdd3","added_by":"auto","created_at":"2026-03-05 20:54:16","extension":"pdf","order_by":1,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":487853,"visible":true,"origin":"","legend":"","description":"","filename":"ALCHbJournalofAutomatedReasoning1.pdf","url":"https://assets-eu.researchsquare.com/files/rs-4818202/v1_covered_cb9125b4-fc78-4d93-9fed-4aa38b8359f2.pdf"}],"financialInterests":"No competing interests reported.","formattedTitle":"A connection method for a defeasible extension of ALCH","fulltext":[],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":false,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":false,"hideJournal":true,"highlight":"","institution":"","isAcceptedByJournal":false,"isAuthorSuppliedPdf":true,"isDeskRejected":"","isHiddenFromSearch":false,"isInQc":false,"isInWorkflow":false,"isPdf":true,"isPdfUpToDate":true,"isWithdrawnOrRetracted":false,"journal":{"display":true,"email":"[email protected]","identity":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true},"keywords":"Connection method, Description logic, Defeasible logics, Web Semantics","lastPublishedDoi":"10.21203/rs.3.rs-4818202/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-4818202/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"The development of proof methods for defeasible description logics (DLs), following those for classical DLs, is mainly based on semantic tableaux.However, the literature offers equally viable alternatives for automated theorem proving, such as the connection method.It consists of a goal-oriented direct proof search method that searches for connections (complementary pairs of literals) in a set of literals organized in clauses called a matrix.This paper presents a connection method for an exception-tolerant family of DLs.In that regard, (i) we use the language of ALCH extended with a typicality operator on concepts and another one on roles; (ii) we revisit the definition of a matrix representation of a knowledge base and establish the conditions for a given axiom to be provable from this matrix with a new normal form (Bi-Typicality Normal Form); (iii) we show how to handle term unification and define a suitable blocking condition in the presence of typicality operators; and (iv) we establish correctness, completeness, and termination of our algorithm.","manuscriptTitle":"A connection method for a defeasible extension of ALCH","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2024-08-27 08:43:25","doi":"10.21203/rs.3.rs-4818202/v1","editorialEvents":[{"type":"communityComments","content":0}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true}}],"origin":"","ownerIdentity":"36d6a44f-98fd-448f-a11a-8282e926e4e0","owner":[],"postedDate":"August 27th, 2024","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"posted","subjectAreas":[],"tags":[],"updatedAt":"2026-03-05T20:54:03+00:00","versionOfRecord":[],"versionCreatedAt":"2024-08-27 08:43:25","video":"","vorDoi":"","vorDoiUrl":"","workflowStages":[]},"version":"v1","identity":"rs-4818202","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-4818202","identity":"rs-4818202","version":["v1"]},"buildId":"qtupq5eGEP_6zYnWcrvyt","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}