@inbook{62701, abstract = {{Learning continuous vector representations for knowledge graphs has significantly improved state-of-the-art performances in many challenging tasks. Yet, deep-learning-based models are only post-hoc and locally explainable. In contrast, learning Web Ontology Language (OWL) class expressions in Description Logics (DLs) is ante-hoc and globally explainable. However, state-of-the-art learners have two well-known lim-itations: scaling to large knowledge graphs and handling missing infor-mation. Here, we present a decision-tree-based learner (tDL) to learn Web Ontology Languages (OWLs) class expressions over large knowl-edge graphs, while imputing missing triples. Given positive and negative example individuals, tDL firstly constructs unique OWL expressions in .SHOIN from concise bounded descriptions of individuals. Each OWL class expression is used as a feature in a binary classification problem to represent input individuals. Thereafter, tDL fits a CART decision tree to learn Boolean decision rules distinguishing positive examples from nega-tive examples. A final OWL expression in.SHOIN is built by traversing the built CART decision tree from the root node to leaf nodes for each positive example. By this, tDL can learn OWL class expressions without exploration, i.e., the number of queries to a knowledge graph is bounded by the number of input individuals. Our empirical results show that tDL outperforms the current state-of-the-art models across datasets. Impor-tantly, our experiments over a large knowledge graph (DBpedia with 1.1 billion triples) show that tDL can effectively learn accurate OWL class expressions, while the state-of-the-art models fail to return any results. Finally, expressions learned by tDL can be seamlessly translated into natural language explanations using a pre-trained large language model and a DL verbalizer.}}, author = {{Demir, Caglar and Yekini, Moshood and Röder, Michael and Mahmood, Yasir and Ngonga Ngomo, Axel-Cyrille}}, booktitle = {{Lecture Notes in Computer Science}}, isbn = {{9783032060655}}, issn = {{0302-9743}}, keywords = {{Decision Tree, OWL Class Expression Learning, Description Logic, Knowledge Graph, Large Language Model, Verbalizer}}, location = {{Porto, Portugal}}, publisher = {{Springer Nature Switzerland}}, title = {{{Tree-Based OWL Class Expression Learner over Large Graphs}}}, doi = {{10.1007/978-3-032-06066-2_29}}, year = {{2025}}, } @article{55236, abstract = {{From 1901 to 1919, Russell persistently maintained that there were two kinds of logic and distinguished between one and the other as mathematical logic and philosophical logic. In this paper, we discuss the concept of philosophical logic, as used by Russell. This was only a tentative program that Russell did not clarify in detail; therefore, our task will be to make it explicit. We shall show that there are three (-and-a-half) kinds of Russellian philosophical logic: (i) “pure logic”; (ii) philosophical logic investigating the logical forms of propositions; (iii) philosophical logic exploring the logical forms of facts: in epistemology and in the external world. In particular, Russell’s program or philosophical logic of the facts of the external world remained less than sketchily outlined. }}, author = {{Milkov, Nikolay}}, journal = {{Athens Journal of Philosophy}}, keywords = {{Russell, mathematical logic, philosophical logic, Wittgenstein}}, number = {{3}}, pages = {{193--209}}, title = {{{Bertrand Russell’s Philosophical Logic and its Logical Forms}}}, doi = {{10.30958/ajphil.2-3-3}}, volume = {{2}}, year = {{2023}}, } @article{45847, abstract = {{Abstract In this paper, we investigate the parameterized complexity of model checking for Dependence and Independence logic, which are well studied logics in the area of Team Semantics. We start with a list of nine immediate parameterizations for this problem, namely the number of disjunctions (i.e. splits)/(free) variables/universal quantifiers, formula-size, the tree-width of the Gaifman graph of the input structure, the size of the universe/team and the arity of dependence atoms. We present a comprehensive picture of the parameterized complexity of model checking and obtain a division of the problem into tractable and various intractable degrees. Furthermore, we also consider the complexity of the most important variants (data and expression complexity) of the model checking problem by fixing parts of the input.}}, author = {{Kontinen, Juha and Meier, Arne and Mahmood, Yasir}}, issn = {{0955-792X}}, journal = {{Journal of Logic and Computation}}, keywords = {{Logic, Hardware and Architecture, Arts and Humanities (miscellaneous), Software, Theoretical Computer Science}}, number = {{8}}, pages = {{1624--1644}}, publisher = {{Oxford University Press (OUP)}}, title = {{{A parameterized view on the complexity of dependence and independence logic}}}, doi = {{10.1093/logcom/exac070}}, volume = {{32}}, year = {{2022}}, } @article{45844, abstract = {{Abstract Abductive reasoning is a non-monotonic formalism stemming from the work of Peirce. It describes the process of deriving the most plausible explanations of known facts. Considering the positive version, asking for sets of variables as explanations, we study, besides the problem of wether there exists a set of explanations, two explanation size limited variants of this reasoning problem (less than or equal to, and equal to a given size bound). In this paper, we present a thorough two-dimensional classification of these problems: the first dimension is regarding the parameterized complexity under a wealth of different parameterizations, and the second dimension spans through all possible Boolean fragments of these problems in Schaefer’s constraint satisfaction framework with co-clones (T. J. Schaefer. The complexity of satisfiability problems. In Proceedings of the 10th Annual ACM Symposium on Theory of Computing, May 1–3, 1978, San Diego, California, USA, R.J. Lipton, W.A. Burkhard, W.J. Savitch, E.P. Friedman, A.V. Aho eds, pp. 216–226. ACM, 1978). Thereby, we almost complete the parameterized complexity classification program initiated by Fellows et al. (The parameterized complexity of abduction. In Proceedings of the Twenty-Sixth AAAI Conference on Articial Intelligence, July 22–26, 2012, Toronto, Ontario, Canada, J. Homann, B. Selman eds. AAAI Press, 2012), partially building on the results by Nordh and Zanuttini (What makes propositional abduction tractable. Artificial Intelligence, 172, 1245–1284, 2008). In this process, we outline a fine-grained analysis of the inherent parameterized intractability of these problems and pinpoint their FPT parts. As the standard algebraic approach is not applicable to our problems, we develop an alternative method that makes the algebraic tools partially available again.}}, author = {{Mahmood, Yasir and Meier, Arne and Schmidt, Johannes}}, issn = {{0955-792X}}, journal = {{Journal of Logic and Computation}}, keywords = {{Logic, Hardware and Architecture, Arts and Humanities (miscellaneous), Software, Theoretical Computer Science}}, number = {{1}}, pages = {{266--296}}, publisher = {{Oxford University Press (OUP)}}, title = {{{Parameterized complexity of abduction in Schaefer’s framework}}}, doi = {{10.1093/logcom/exaa079}}, volume = {{31}}, year = {{2021}}, } @inbook{35811, author = {{Biehler, Rolf and Durand-Guerrier, Viviane}}, booktitle = {{Proceedings of the Third Conference of the International Network for Didactic Research in University Mathematics (INDRUM 2020, 12-19 September 2020)}}, editor = {{Hausberger, T. and Bosch, M. and Chelloughi, F.}}, keywords = {{Number Theory, Algebra, Discrete Mathematics, Logic, Research in University Mathematics Edcuation}}, pages = {{283--287}}, publisher = {{University of Carthage and INDRUM}}, title = {{{University Mathematics Didactic Research on Number Theory, Algebra, Discrete Mathematics, Logic}}}, year = {{2020}}, } @article{3343, abstract = {{In this paper we consider an extended variant of query learning where the hidden concept is embedded in some Boolean circuit. This additional processing layer modifies query arguments and answers by fixed transformation functions which are known to the learner. For this scenario, we provide a characterization of the solution space and an ordering on it. We give a compact representation of the minimal and maximal solutions as quantified Boolean formulas and we adapt the original algorithms for exact learning of specific classes of propositional formulas.}}, author = {{Bubeck, Uwe and Kleine Büning, Hans}}, issn = {{0004-3702}}, journal = {{Artificial Intelligence}}, keywords = {{Query learning, Propositional logic}}, pages = {{246 -- 257}}, publisher = {{Elsevier}}, title = {{{Learning Boolean Specifications}}}, doi = {{10.1016/j.artint.2015.09.003}}, year = {{2015}}, } @inproceedings{10677, author = {{Ho, Nam and Kaufmann, Paul and Platzner, Marco}}, booktitle = {{2014 {IEEE} Intl. Conf. on Evolvable Systems (ICES)}}, keywords = {{Linux, cache storage, embedded systems, granular computing, multiprocessing systems, reconfigurable architectures, Leon3 SPARe processor, custom logic events, evolvable-self-adaptable processor cache, fine granular profiling, integer unit events, measurement infrastructure, microarchitectural events, multicore embedded system, perf_event standard Linux performance measurement interface, processor properties, run-time reconfigurable memory-to-cache address mapping engine, run-time reconfigurable multicore infrastructure, split-level caching, Field programmable gate arrays, Frequency locked loops, Irrigation, Phasor measurement units, Registers, Weaving}}, pages = {{31--37}}, title = {{{Towards self-adaptive caches: A run-time reconfigurable multi-core infrastructure}}}, doi = {{10.1109/ICES.2014.7008719}}, year = {{2014}}, } @article{17663, abstract = {{In this paper, we define and study a new problem, referred to as the Dependent Unsplittable Flow Problem (D-UFP). We present and discuss this problem in the context of large-scale powerful (radar/camera) sensor networks, but we believe it has important applications on the admission of large flows in other networks as well. In order to optimize the selection of flows transmitted to the gateway, D-UFP takes into account possible dependencies between flows. We show that D-UFP is more difficult than NP-hard problems for which no good approximation is known. Then, we address two special cases of this problem: the case where all the sensors have a shared channel and the case where the sensors form a mesh and route to the gateway over a spanning tree.}}, author = {{Cohen, R. and Nudelman, I. and Polevoy, Gleb}}, issn = {{1063-6692}}, journal = {{Networking, IEEE/ACM Transactions on}}, keywords = {{Approximation algorithms, Approximation methods, Bandwidth, Logic gates, Radar, Vectors, Wireless sensor networks, Dependent flow scheduling, sensor networks}}, number = {{5}}, pages = {{1461--1471}}, title = {{{On the Admission of Dependent Flows in Powerful Sensor Networks}}}, doi = {{10.1109/TNET.2012.2227792}}, volume = {{21}}, year = {{2013}}, } @inproceedings{10620, author = {{Anwer, Jahanzeb and Meisner, Sebastian and Platzner, Marco}}, booktitle = {{Reconfigurable Computing and FPGAs (ReConFig), 2013 International Conference on}}, keywords = {{fault tolerant computing, field programmable gate arrays, logic design, reliability, BYU-LANL tool, DRM tool flow, FPGA based hardware designs, avionic application, device technologies, dynamic reliability management, fault-tolerant operation, hardware designs, reconfiguring reliability levels, space applications, Field programmable gate arrays, Hardware, Redundancy, Reliability engineering, Runtime, Tunneling magnetoresistance}}, pages = {{1--6}}, title = {{{Dynamic reliability management: Reconfiguring reliability-levels of hardware designs at runtime}}}, doi = {{10.1109/ReConFig.2013.6732280}}, year = {{2013}}, } @inbook{33825, abstract = {{This article describes our approach for the specification and verification of production automation systems with real-time properties. We focus on the graphical MFERT notation and RT-OCL (Real-Time Object Constraint Language) for the specification of state-oriented real-time properties. RT-OCL is an extension of the Object Constraint Language (OCL) that is part of the Unified Modeling Language (UML). We introduce the formal semantics of RT-OCL based on a formal model of UML Class and State Diagrams and provide a mapping to temporal logics. The applicability of our approach is demonstrated by the case study of a manufacturing system with automated guided vehicles.}}, author = {{Flake, Stephan and Müller, Wolfgang and Pape, Ulrich and Ruf, Jürgen}}, booktitle = {{Integration of Software Specification Techniques for Applications in Engineering}}, editor = {{Ehrig, Hartmut and Damm, Werner and Desel, Jörg and Große-Rhode, Martin and Reif, Wolfgang and Schnieder, Eckehard and Westkämper, Engelbert}}, isbn = {{978-3-540-27863-4}}, keywords = {{Model Check, Temporal Logic, Object Constraint Language, Abstract Syntax, Temporal Logic Formula}}, pages = {{206--226}}, publisher = {{Springer-Verlag}}, title = {{{Specification and Formal Verification of Temporal Properties of Production Automation Systems}}}, doi = {{10.1007/978-3-540-27863-4_13}}, volume = {{3147}}, year = {{2004}}, } @inproceedings{39061, abstract = {{This article presents an approach, which combines theorem proving-based refinement with model checking for state based real-time systems. Our verification flow starts from UML state diagrams, which are translated to the formal B language and are model checked for real-time properties. By means of the B language and a B theorem prover, refined state diagrams are verified against their abstract representation. The approach is presented by means of the refinement of a digital echo cancellation unit.}}, author = {{Krupp, Alexander and Müller, Wolfgang and Oliver, Ian}}, booktitle = {{Proceedings of DATE’04 Designers' Forum}}, isbn = {{0-7695-2085-5}}, keywords = {{Echo cancellers, Logic, Unified modeling language, Automata, Data structures, Boolean functions, Electronic design automation and methodology, Prototypes, Specification languages, Constraint theory}}, title = {{{Formal Refinement and Model Checking of An Echo Cancellation Unit}}}, doi = {{10.1109/DATE.2004.1269214}}, year = {{2004}}, } @inproceedings{39069, abstract = {{We present the syntax and semantics of a past- and future-oriented temporal extension of the Object Constraint Language (OCL). Our extension supports designers to express time-bounded properties over a state-oriented UML model of a system under development. The semantics is formally defined over the system states of a mathematical object model. Additionally, we present a mapping to Clocked Linear Temporal Logic (Clocked LTL) formulae, which is the basis for further application in verification with model checking. We demonstrate the applicability of the approach by the example of a buffer specification in the context of a production system.}}, author = {{Flake, Stephan and Müller, Wolfgang}}, booktitle = {{Proceedings of SEFM´04}}, isbn = {{0-7695-2222-X}}, keywords = {{Unified modeling language, Logic, Clocks, Boolean functions, Application software, Time factors, Real time systems, Formal verification, Buffer storage, Software packages}}, publisher = {{IEEE}}, title = {{{Past- and Future-Oriented Time-Bound Temporal Properties with OCL}}}, doi = {{10.1109/SEFM.2004.1347516}}, year = {{2004}}, } @inbook{34447, abstract = {{The Object Constraint Language (OCL) was introduced to support the specification of constraints for UML diagrams and is mainly used to formulate invariants and operation pre- and postconditions. Though OCL is also applied in behavioral diagrams, e.g., as guards for state transitions, it is currently not possible to specify constraints concerning the dynamic behavior and timing properties of such diagrams. This article discusses OCL’s application for the dynamic behavior of UML Statechart diagrams and presents an OCL extension for specification of state-oriented time-bounded constraints.We introduce operations to extract state configurations from diagrams and define additional predicates over states and state configurations. The semantics of our OCL extension is given by employing time-bounded Computational Tree Logic (CTL) formulae. An example of a flexible manufacturing system with automated guided vehicles demonstrates the application of our extension.}}, author = {{Flake, Stephan and Müller, Wolfgang}}, booktitle = {{Advances in Object Modelling with the OCL}}, editor = {{Clark, T. and Warmer, J.}}, isbn = {{978-3-540-45669-8}}, keywords = {{Model Check Temporal Logic Object Constraint Language Execution Path Kripke Structure}}, pages = {{150 -- 171}}, publisher = {{Springer-Verlag}}, title = {{{An OCL Extension for Real-Time Constraints}}}, doi = {{10.1007/3-540-45669-4_8}}, year = {{2002}}, } @inproceedings{39382, abstract = {{We present a rigorous but transparent semantics definition of the SpecC language that covers the execution of SpecC behaviors and their interaction with the kernel process. The semantics include wait, wait for, par, and try statements as they are introduced in SpecC. We present our definition in form of distributed abstract state machine (ASM) rules strictly following the lines of the SpecC Language Reference Manual. We mainly see our formal semantics in three application areas. First, it is a concise, unambiguous description for documentation and standardization. Second, it applies as a high-level, pseudo code-oriented specification for the implementation of a SpecC simulator. Finally, it is a first step for SpecC synthesis in order to identify similar concepts with other languages like VHDL and SystemC for the definition of common patterns and language subsets.}}, author = {{Müller, Wolfgang and Dömer, Rainer and Gerstlauer, Andreas}}, booktitle = {{Proceedings of the ISSS02}}, isbn = {{1-58113-576-9}}, keywords = {{Standardization, Kernel, Permission, Formal verification, Logic functions, Documentation, Reasoning about programs, Specification languages, Formal specifications, Software systems}}, title = {{{The Formal Execution Semantics of SpecC}}}, doi = {{10.1145/581199.581234 }}, year = {{2002}}, } @inproceedings{39403, abstract = {{The Unified Modeling Language (UML) has received wide acceptance as a standard language in the field of software specification by means of different diagram types. In a recent version of UML, the textual Object Constraint Language (OCL) was introduced to support specification of constraints for UML models. But OCL currently does not provide sufficient means to specify constraints over the dynamic behavior of a model. This article presents an OCL extension that is consistent with current OCL and enables modelers to specify state-related time-bounded constraints. We consider the case study of a flexible manufacturing system and identify typical real-time constraints. The constraints are presented in our temporal OCL extension as well as in temporal logic formulae. For general application, we define a semantics of our OCL extension by means of a time-bounded temporal logic based on Computational Tree Logic (CTL).}}, author = {{Flake, Stephan and Müller, Wolfgang}}, booktitle = {{Proceedings of HICSS-35}}, isbn = {{0-7695-1435-9}}, keywords = {{Unified modeling language, Logic, Formal verification, Real time systems, Programming profession, Vehicle dynamics, Software standards, Flexible manufacturing systems, Electronics industry, Protocols}}, location = {{Big Island, HI, USA }}, title = {{{Specification of Real-Time Properties for UML Models}}}, doi = {{10.1109/HICSS.2002.994469}}, year = {{2002}}, } @inproceedings{39421, abstract = {{We present a rigorous but transparent semantics definition of SystemC that covers method, thread, and clocked thread behavior as well as their interaction with the simulation kernel process. The semantics includes watching statements, signal assignment, and wait statements as they are introduced in SystemC V1.O. We present our definition in form of distributed Abstract State Machines (ASMs) rules reflecting the view given in the SystemC User's Manual and the reference implementation. We mainly see our formal semantics as a concise, unambiguous, high-level specification for SystemC-based implementations and for standardization. Additionally, it can be used as a sound basis to investigate SystemC interoperability with Verilog and VHDL.}}, author = {{Müller, Wolfgang and Ruf, Jürgen and Hoffmann, D. W. and Gerlach, Joachim and Kropf, Thomas and Rosenstiehl, W.}}, booktitle = {{Proceedings of the Design, Automation, and Test in Europe (DATE’01)}}, isbn = {{0-7695-0993-2}}, keywords = {{Yarn, Formal verification, Kernel, Hardware design languages, Electronic design automation and methodology, Algebra, Computational modeling, Logic functions, Computer languages, Clocks}}, publisher = {{IEEE}}, title = {{{The Simulation Semantics of SystemC}}}, doi = {{10.1109/DATE.2001.915002}}, year = {{2001}}, }