Making Theory Reasoning Simpler

Reasoning with quantifiers and theories is at the core of many applications in program analysis and verification. Whilst the problem is undecidable in general and hard in practice, we have been making large pragmatic steps forward. Our previous work proposed an instantiation rule for theory reasoning that produced pragmatically useful instances. Whilst this led to an increase in performance, it had its limitations as the rule produces ground instances which (i) can be overly specific, thus not useful in proof search, and (ii) contribute to the already problematic search space explosion as many new instances are introduced. This paper begins by introducing that specifically addresses these two concerns as it produces general solutions and it is a simplification rule, i.e. it replaces an existing clause by a ‘simpler’ one. Encouraged by initial success with this new rule, we performed an experiment to identify further common cases where the complex structure of theory terms blocked existing methods. This resulted in four further simplification rules for theory reasoning. The resulting extensions are implemented in the Vampire theorem prover and evaluated on SMT-LIB, showing that the new extensions result in a considerable increase in the number of problems solved, including 90 problems unsolved by state-of-the-art SMT solvers.

Experimenting with Theory Instantiation in Vampire

Theory instantiation tackles the problem of theory reasoning with quantifiers in Vam- pire using an SMT solver. In contrast to AVATAR modulo theories it works locally by instantiating a clause such that its pure theory part becomes inconsistent and can be deleted. We report on the challenges when adding instantiation for the theory of arrays.

The limits of conjecture: Political liberalism, counter-radicalisation and unreasonable religious views

Originally proposed by John Rawls, the idea of reasoning from conjecture is popular among the proponents of political liberalism in normative political theory. Reasoning from conjecture consists in discussing with fellow citizens who are attracted to illiberal and antidemocratic ideas by focusing on their religious or otherwise comprehensive doctrines, attempting to convince them that such doctrines actually call for loyalty to liberal democracy. Our goal is to criticise reasoning from conjecture as a tool aimed at persuasion and, in turn, at improving the stability of liberal democratic institutions. To pursue this goal, we use as case study real-world efforts to counter-radicalise at-risk Muslim citizens, which, at first glance, reasoning from conjecture seems well-placed to contribute to. This case study helps us to argue that the supporters of reasoning from conjecture over-intellectualise opposition to liberal democracy and what societies can do to counter it. Specifically, they (i) underestimate how few members of society can effectively perform reasoning from conjecture; (ii) overlook that the burdens of judgement, a key notion for political liberals, highlight how dim the prospects of reasoning from conjecture are and (iii) do not pay attention to the causes of religious persons’ opposition to liberal democracy. However, not everything is lost for political liberals, provided that they redirect attention to different and under-researched resources contained in Rawls’s theory. In closing, we briefly explain how such resources are much better placed than reasoning from conjecture to provide guidance relative to counter-radicalisation in societies (i) populated by persons who do not generally hold anything close to a fully worked out and internally consistent comprehensive doctrine and (ii) where political institutions should take responsibility for at least part of the existing alienation from liberal democratic values.

PROFIL KESALAHAN PEMAHAMAN KONSEP CAHAYA PADA SISWA KELAS V SEKOLAH DASAR

This research describes the error concept of light profile in grade V students of SD N Srondol Wetan 02. The error concept made by the students need to be analyzed further in order to get a clear and detailed description of the students' weaknesses in understanding the concept of light and used as a consideration of learning in the business improve the quality of the learning process. Subjects amounted to four students who error concept. Data collection techniques use documentation, tests, observations, and interviews. Analysis of qualitative data through three stages of data reduction, presenting data, and concluding. The results showed: (1) KP-1 students have low sample indicator but KP-2 students actually have good example indicator; 2) errors concepts occur in the concept of light sources, light-permeable objects, light refraction, light of light degradation, and objects utilizing the nature of light; (3) the factors causing error concept of students' are student only learning only the IPA textbook from the school and the notebook from the teacher, the student assumes that all the concepts derived from experience and natural phenomena are true without re-examining the correct theory, reasoning, incomplete and inaccurate reading of textbooks or problems of understanding, as well as the limitations of language in understanding the concept of light.

Hybrid metabolic network completion

Metabolic networks play a crucial role in biology since they capture all chemical reactions in an organism. While there are networks of high quality for many model organisms, networks for less studied organisms are often of poor quality and suffer from incompleteness. To this end, we introduced in previous work an answer set programming (ASP)-based approach to metabolic network completion. Although this qualitative approach allows for restoring moderately degraded networks, it fails to restore highly degraded ones. This is because it ignores quantitative constraints capturing reaction rates. To address this problem, we propose a hybrid approach to metabolic network completion that integrates our qualitative ASP approach with quantitative means for capturing reaction rates. We begin by formally reconciling existing stoichiometric and topological approaches to network completion in a unified formalism. With it, we develop a hybrid ASP encoding and rely upon the theory reasoning capacities of the ASP system clingo for solving the resulting logic program with linear constraints over reals. We empirically evaluate our approach by means of the metabolic network of Escherichia coli. Our analysis shows that our novel approach yields greatly superior results than obtainable from purely qualitative or quantitative approaches.

Checkable Proofs for First-Order Theorem Proving

Inspired by the success of the DRAT proof format for certification of boolean satisfiability (SAT),we argue that a similar goal of having unified automatically checkable proofs should be soughtby the developers of automated first-order theorem provers (ATPs). This would not onlyhelp to further increase assurance about the correctness of prover results,but would also be indispensable for tools which rely on ATPs,such as ``hammers'' employed within interactive theorem provers.The current situation, represented by the TSTP format is unsatisfactory,because this format does not have a standardised semantics and thus cannot be checked automatically.Providing such semantics, however, is a challenging endeavour. One would ideallylike to have a proof format which covers only-satisfiability-preserving operations such as Skolemisationand is versatile enough to encompass various proving methods (i.e. not just superposition)or is perhaps even open ended towards yet to be conceived methods or at least easily extendable in principle.Going beyond pure first-order logic to theory reasoning in the style of SMT orbeyond proofs to certification of satisfiability are further interesting challenges.Although several projects have already provided partial solutions in this direction,we would like to use the opportunity of ARCADE to further promote the idea andgather critical mass needed for its satisfactory realisation.