the proceedings contain 31 papers. the special focus in this conference is on logic for programming, artificial intelligence and reasoning. the topics include: Automated theorem Provers Help Improve Large Language Mod...
the proceedings contain 31 papers. the special focus in this conference is on logic for programming, artificial intelligence and reasoning. the topics include: Automated theorem Provers Help Improve Large Language Model reasoning;reasoning About Group Polarization: From Semantic Games to Sequent Systems;saturating Sorting without Sorts;waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper);Automatic Detection of Vulnerable Variables for CTL Properties of Programs;a Tool for reasoning about Trust and Belief;efficient Simulation for Hardware Model Checking;VIRAS: Conflict-Driven Quantifier Elimination Integer-Real Arithmetic;tree-Verifiable Graph Grammar;Hybrid Intersection Types for PCF;Automatic Bit-and Memory-Precise Verification of eBPF Code;scaling CheckMate for Game-theoretic Security;On Translations of Epsilon Proofs to LK;a Generic Deskolemization Strategy;first Experiments with Neural cvc5;rewriting and Inductive reasoning;herbrand’s theorem in Inductive Proofs;experiments with Choice in Dependently-Typed Higher-Order logic;Certifying Incremental SAT Solving;a Simple Token Game and its logic;prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery;deep Inference in Proof Search: the Need for Shallow Inference;symbolic Realisation of Epistemic Processes;Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition;fuzzy Datalog∃ over Arbitrary t-Norms;Verifying SQL Queries using theories of Tables and Relations;confluence for Proof Nets via Parallel Cut Elimination;automated Synthesis of Decision Lists for Polynomial Specifications over Integers.
Most high-end automated theorem provers for first order logic (FOL) split available time between short runs of a large portfolio of search strategies. these runs are typically independent and can be parallelized to ex...
详细信息
In this paper we present the proof that there is no elementary translation from cut-free derivations in the sequent calculus variant of the epsilon calculus to LK-proofs with bounded cut-complexity. this is a partial ...
详细信息
We introduce a simple game of resource-conscious reasoning. In this two-player game, players P and O place tokens of positive and negative polarity onto a game board according to certain rules. P wins if she manages t...
详细信息
An inductive proof can be represented as a proof schema, i.e. as a parameterized sequence of proofs defined in a primitive recursive way. A corresponding cut-elimination method, called schematic CERES, can be used to ...
详细信息
We propose an approach to infer the critical logic blocks contained within student submissions that can influence the passing or failing of individual exercises in introductory programming courses. Given a programming...
详细信息
ISBN:
(纸本)9783031642982;9783031642999
We propose an approach to infer the critical logic blocks contained within student submissions that can influence the passing or failing of individual exercises in introductory programming courses. Given a programming exercise, we extract critical logic blocks from the abstract syntax trees (ASTs) of its submissions and use a bag-of-words approach to train a decision tree classifier to predict the pass/failure of a submission given the logic blocks present in its AST. We apply this technique to two streams of an introductory Python programming course for high-school students, constructing decision trees for 66 programming exercises based on several thousand submissions for each exercise. We obtain classifiers with F1 scores of 92.4% for the beginners and 88.2% for the intermediate stream. these trained models are highly interpretable and can provide a visualisation of the key logic blocks that are critical in the pass/failure of a problem. We explain how the models can assist educators in understanding the common valid approaches or failed attempts carried out by students when tackling a specific problem, and they may also serve as a guide for suggesting hints to struggling students.
Weather forecasting is important for saving lives, protecting property, and supporting economic activities. It provides timely warnings for severe weather, improves agricultural planning, and aids in disaster manageme...
详细信息
ISBN:
(纸本)9783031742088;9783031742095
Weather forecasting is important for saving lives, protecting property, and supporting economic activities. It provides timely warnings for severe weather, improves agricultural planning, and aids in disaster management. Neural networks and deep learning methods can achieve impressive accuracy in weather prediction, but their black-box nature lacks in explainability. To address this limitation, we investigated the potential of FastLAS, an Inductive logicprogramming (ILP) framework, to produce reliable and, more important, explainable weather predictions. FastLAS learns ASP programs whose syntax and structural semantics resemble natural human language, making them easily understandable and interpretable by humans. the supportedness of stable models allows a clear explanation of the predictions. Our empirical evaluation on data from an Italian weather forecasting center shows that our approach is capable of learning predictive models from small dataset (a few samples instead of the thousands needed by neural networks) achieving an accuracy higher than statistical machine learning base lines.
Recently an extension to higher-order logic — called DHOL — was introduced, enriching the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice ...
详细信息
Group polarization, the phenomenon where individuals become more extreme after interacting, has been gaining attention, especially withthe rise of social media shaping peo-ple’s opinions. Recent interest has emerged...
详细信息
One of the main challenges in the area of Neuro-Symbolic AI is to perform logical reasoning in the presence of both neural and symbolic data. this requires combining heterogeneous data sources such as knowledge graphs...
详细信息
暂无评论