Recently, we showed how to use control-flow refinement (CFR) to improve automatic complexity analysis of integer programs. While up to now CFR was limited to classical programs, in this paper we extend CFR to probabil...
详细信息
ISBN:
(数字)9783031634987
ISBN:
(纸本)9783031634970;9783031634987
Recently, we showed how to use control-flow refinement (CFR) to improve automatic complexity analysis of integer programs. While up to now CFR was limited to classical programs, in this paper we extend CFR to probabilistic programs and show its soundness for complexity analysis. To demonstrate its benefits, we implemented our new CFR technique in our complexity analysis tool KoAT.
this paper describes a new format for representing Tarskian-style interpretations for formulae in typed first-order logic, using the TPTP TF0 language. It further describes a technique and an implemented tool for veri...
详细信息
Bachmair's and Ganzinger's abstract redundancy concept for the Superposition Calculus justifies almost all operations that are used in superposition provers to delete or simplify clauses, and thus to keep the ...
详细信息
ISBN:
(数字)9783031634987
ISBN:
(纸本)9783031634970;9783031634987
Bachmair's and Ganzinger's abstract redundancy concept for the Superposition Calculus justifies almost all operations that are used in superposition provers to delete or simplify clauses, and thus to keep the clause set manageable. Typical examples are tautology deletion, subsumption deletion, and demodulation, and with a more refined definition of redundancy joinability and connectedness can be covered as well. the notable exception is Destructive Equality Resolution, that is, the replacement of a clause x not approximate to t boolean OR C with x is not an element of vars(t) by C{x -> t}. this operation is implemented in state-of-the-art provers, and it is clearly useful in practice, but little is known about how it affects refutational completeness. We demonstrate on the one hand that the naive addition of Destructive Equality Resolution to the standard abstract redundancy concept renders the calculus refutationally incomplete. On the other hand, we present several restricted variants of the Superposition Calculus that are refutationally complete even with Destructive Equality Resolution.
Given a finite consistent set of ground literals, we present an algorithm that generates a complete first-order logic interpretation, i.e., an interpretation for all ground literals over the signature and not just tho...
详细信息
ISBN:
(数字)9783031634987
ISBN:
(纸本)9783031634970;9783031634987
Given a finite consistent set of ground literals, we present an algorithm that generates a complete first-order logic interpretation, i.e., an interpretation for all ground literals over the signature and not just those in the input set, that is also a model for the input set. the interpretation is represented by first-order linear literals. It can be effectively used to evaluate clauses. A particular application are SCL stuck states. the SCL (Simple Clause Learning) calculus always computes with respect to a finite number of ground literals. It then finds either a contradiction or a stuck state being a model with respect to the considered ground literals. Our algorithm builds a complete literal interpretation out of such a stuck state model that can then be used to evaluate the clause set. If all clauses are satisfied an overall model has been found. If it does not satisfy some clause, this information can be effectively explored to extend the scope of ground literals considered by SCL.
Preparing healthy and delicious meals requires knowledge about the process, nutritional properties of the ingredients, and their combinations. When we face the need for substitution in a dish, e.g., for allergic or di...
详细信息
the proceedings contain 15 papers. the special focus in this conference is on Practical Aspects of Declarative Languages. the topics include: the Scenic Route to Deforestation: An Exercise in Applying Parametrici...
ISBN:
(纸本)9783031849237
the proceedings contain 15 papers. the special focus in this conference is on Practical Aspects of Declarative Languages. the topics include: the Scenic Route to Deforestation: An Exercise in Applying Parametricity in Curry;MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs;SM-Based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic;a Practical Approach to Handling Tabular Data in logic;automated Playing of Survival Video Games with Commonsense reasoning;checking Concurrency Coding Rules;A Weighted Bipolar Argumentation Framework and Its ASP-Based Implementation;haskell Based Spreadsheets;Leveraging LLM reasoning with Dual Horn Programs;ASP for Language Documentation and Reclamation: A Derivational Stemming Tool for Myaamia;Enhancing a Hierarchical Graph Rewriting Language Based on MELL Cut Elimination;c3G: Causally Constrained Counterfactual Generation;exploring Answer Set programming for Provenance Graph-Based Cyber threat Detection: A Novel Approach.
Aside from the necessary learning skills of logical thinking, problem-solving, and creativity, undergraduate students in the programming discipline must also be self-motivated because these abilities enable them to ov...
详细信息
ISBN:
(纸本)9798400708732
Aside from the necessary learning skills of logical thinking, problem-solving, and creativity, undergraduate students in the programming discipline must also be self-motivated because these abilities enable them to overcome obstacles and achieve success. In the digital learning era, a pedagogical approach emphasizing inquiry and collaborative approaches can enhance students' programming skills anywhere and anytime. As a result, this research aims to investigate the effects of collaborative learning on academic achievement and motivation by managing ubiquitous learning in computer courses at three universities in northern thailand using a collaborative inquiry-based approach. the learning environment allowed students to practice independently using the instructor-provided content and exercises. then, as part of group learning, students gave advice and shared knowledge until they found the best solution. Following class, the instructor discussed the merits of each group's responses with all students. Students were then asked to repeat the questions to ensure they completely understood the logical reasoning and problem-solving process. According to the findings, ubiquitous learning management based on collaborative inquiry-based approaches could help them learn more effectively, with higher learning achievement and motivation. the study's findings inspire further research into creating a collaborative digital learning environment in computer education, particularly from the standpoint of ubiquitous learning.
We propose a definition of common explanation for the label shared by a group of observations described as first order interpretations, and provide algorithms to enumerate minimal common explanations. this was motivat...
详细信息
ISBN:
(纸本)9783031450716;9783031450723
We propose a definition of common explanation for the label shared by a group of observations described as first order interpretations, and provide algorithms to enumerate minimal common explanations. this was motivated by explaining how performing some action, for instance a card played during a card game play, results in winning a maximum total reward at the end of the trajectory. As there are various ways to reach this reward, each associated to a group of trajectories, we propose to first build groups of trajectories and then build minimal common explanations for each group. the whole method is illustrated on a simplified Bridge game.
the European Erasmus+ project ARC - automatedreasoning in the Class aims at improving the academic education in disciplines related to Computational logic by using automatedreasoning tools. We present the technical ...
详细信息
ISBN:
(纸本)9783031166815;9783031166808
the European Erasmus+ project ARC - automatedreasoning in the Class aims at improving the academic education in disciplines related to Computational logic by using automatedreasoning tools. We present the technical aspects of the tools as well as our education experiments, which took place mostly in virtual lectures due to the COVID pandemics. Our education goals are: to support the virtual interaction between teacher and students in the absence of the blackboard, to explain the basic Computational logic algorithms, to study their implementation in certain programming environments, to reveal the main relationships between logic and programming, and to develop the proof skills of the students. For the introductory lectures we use some programs in C and in Mathematica in order to illustrate normal forms, resolution, and DPLL (Davis-Putnam-Logemann-Loveland) with its Chaff version, as well as an implementation of sequent calculus in the theorema system. Furthermore we developed special tools for SAT (propositional satisfiability), some based on the original methods from the partners, including complex tools for SMT (Satisfiability Modulo theories) that allow the illustration of various solving approaches. An SMT related approach is natural-style proving in Elementary Analysis, for which we developed and interesting set of practical heuristics. For more advanced lectures on rewrite systems we use the Coq programming and proving environment, in order on one hand to demonstrate programming in functional style and on the other hand to prove properties of programs. Other advanced approaches used in some lectures are the deduction based synthesis of algorithms and the techniques for program transformation.
the proceedings contain 144 papers. the topics discussed include: towards continuous development for quantum programming in decentralized IoT environments;automated extension-based penetration testing for web vulnerab...
the proceedings contain 144 papers. the topics discussed include: towards continuous development for quantum programming in decentralized IoT environments;automated extension-based penetration testing for web vulnerabilities;addressing imbalanced data in predicting injury severity after traffic crashes: a comparative analysis of machine learning models;short-term glucose prediction in type 1 diabetes;an implementation, evaluation and validation of a dynamic fire and conflagration risk indicator for wooden homes;navigating the local transport gap: a comprehensive development proposal for a real-time location service application;addressing local and regional recharging demand: allocation of charging stations through iterative route analysis;wearable solution for health monitoring of car drivers;and simulating incident management team response and performance.
暂无评论