Complexity of translations from resolution to sequent calculus

2019 ◽  
Vol 29 (8) ◽  
pp. 1061-1091
Author(s):  
GISELLE REIS ◽  
BRUNO WOLTZENLOGEL PALEO
Keyword(s):  
Automated Reasoning ◽  
Theoretical Basis ◽  
Automated Theorem Proving ◽  
Proof Theory ◽  
Sequent Calculus ◽  
Formal Proof ◽  
Human Beings ◽  
Proof Systems ◽  
Translation Methods ◽  
Resolution Calculus

Resolution and sequent calculus are two well-known formal proof systems. Their differences make them suitable for distinct tasks. Resolution and its variants are very efficient for automated reasoning and are in fact the theoretical basis of many theorem provers. However, being intentionally machine oriented, the resolution calculus is not as natural for human beings and the input problem needs to be pre-processed to clause normal form. Sequent calculus, on the other hand, is a modular formalism that is useful for analysing meta-properties of various logics and is, therefore, popular among proof theorists. The input problem does not need to be pre-processed, and proofs are more detailed. However, proofs also tend to be larger and more verbose. When the worlds of proof theory and automated theorem proving meet, translations between resolution and sequent calculus are often necessary. In this paper, we compare three translation methods and analyse their complexity.

scholarly journals Generalized quantification as substructural logic

1996 ◽  
Vol 61 (3) ◽  
pp. 1006-1044 ◽  
Author(s):  
Natasha Alechina ◽  
Michiel Van Lambalgen
Keyword(s):  
Proof Theory ◽  
Sequent Calculus ◽  
Substructural Logic ◽  
Generalized Quantifiers ◽  
Accessibility Relation ◽  
Dependence Relation ◽  
Structural Rules ◽  
First Order ◽  
Proof Systems ◽  
Structured Objects

AbstractWe show how sequent calculi for some generalized quantifiers can be obtained by generalizing the Herbrand approach to ordinary first order proof theory. Typical of the Herbrand approach, as compared to plain sequent calculus, is increased control over relations of dependence between variables. In the case of generalized quantifiers, explicit attention to relations of dependence becomes indispensible for setting up proof systems. It is shown that this can be done by turning variables into structured objects, governed by various types of structural rules. These structured variables are interpreted semantically by means of a dependence relation. This relation is an analogue of the accessibility relation in modal logic. We then isolate a class of axioms for generalized quantifiers which correspond to first-order conditions on the dependence relation.

scholarly journals The Method of Socratic Proofs Meets Correspondence Analysis

2019 ◽  
Vol 48 (2) ◽  
pp. 99-116
Author(s):  
Dorota Leszczyńska-Jasion ◽  
Yaroslav Petrukhin ◽  
Vasilyi Shangin
Keyword(s):  
Correspondence Analysis ◽  
Boolean Functions ◽  
Propositional Logic ◽  
Sequent Calculus ◽  
Sequent Calculi ◽  
Classical Propositional Logic ◽  
Logic Of Questions ◽  
Proof Systems

The goal of this paper is to propose correspondence analysis as a technique for generating the so-called erotetic (i.e. pertaining to the logic of questions) calculi which constitute the method of Socratic proofs by Andrzej Wiśniewski. As we explain in the paper, in order to successfully design an erotetic calculus one needs invertible sequent-calculus-style rules. For this reason, the proposed correspondence analysis resulting in invertible rules can constitute a new foundation for the method of Socratic proofs. Correspondence analysis is Kooi and Tamminga's technique for designing proof systems. In this paper it is used to consider sequent calculi with non-branching (the only exception being the rule of cut), invertible rules for the negation fragment of classical propositional logic and its extensions by binary Boolean functions.

Simulating Crime Events and Crime Patterns in a RA/CA Model

2005 ◽  
pp. 197-213 ◽  
Author(s):  
Lin Liu ◽  
Xuguang Wang ◽  
John Eck ◽  
Jun Liang
Keyword(s):  
Simulation Model ◽  
Theoretical Basis ◽  
Psychological Impact ◽  
Routine Activities ◽  
Human Beings ◽  
Data Set ◽  
Crime Patterns ◽  
State Variable ◽  
Ca Model ◽  
Experimental Runs

This chapter presents an innovative approach for simulating crime events and crime patterns. The theoretical basis of the crime simulation model is routine activities (RA) theory. Offenders, targets and crime places, the three basic elements of routine activities, are modeled as individual agents. The properties and behaviors of these agents change in space and time. The interactions of these three types of agents are modeled in a cellular automaton (CA). Tension, measuring the psychological impact of crime events to human beings, is the state variable of the CA. The model, after being calibrated by using a real crime data set in Cincinnati, is able to generate crime patterns similar to real patterns. Results from experimental runs of the model conform to known criminology theories. This type of RA/CA simulation model has the potential of being used to test new criminology theories and hypotheses.

PROOF SYSTEMS FOR VARIOUS FDE-BASED MODAL LOGICS

2019 ◽  
Vol 13 (4) ◽  
pp. 720-747
Author(s):  
SERGEY DROBYSHEVICH ◽  
HEINRICH WANSING
Keyword(s):  
Modal Logic ◽  
Sequent Calculus ◽  
Axiom System ◽  
Modal Logics ◽  
Cut Elimination ◽  
Proof Systems ◽  
Image Position ◽  
Axiomatic Extension

AbstractWe present novel proof systems for various FDE-based modal logics. Among the systems considered are a number of Belnapian modal logics introduced in Odintsov & Wansing (2010) and Odintsov & Wansing (2017), as well as the modal logic KN4 with strong implication introduced in Goble (2006). In particular, we provide a Hilbert-style axiom system for the logic $BK^{\square - } $ and characterize the logic BK as an axiomatic extension of the system $BK^{FS} $. For KN4 we provide both an FDE-style axiom system and a decidable sequent calculus for which a contraction elimination and a cut elimination result are shown.

scholarly journals TacticToe: Learning to Reason with HOL4 Tactics

10.29007/ntlb ◽  
2018 ◽  
Author(s):  
Thibault Gauthier ◽  
Cezary Kaliszyk ◽  
Josef Urban
Keyword(s):  
Machine Learning ◽  
Automated Reasoning ◽  
Formal Proof ◽  
Small Scale ◽  
Proof Assistant ◽  
Proof Assistants ◽  
A Algorithm ◽  
Learning To Reason ◽  
Traditional Proof ◽  
Selection Of

Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such “hammer” techniques complement traditional proof assistant automation as implemented by tactics and decision procedures. In this paper we present a unified proof assistant automation approach which attempts to automate the selection of appropriate tactics and tactic-sequences combined with an optimized small-scale hammering approach. We implement the technique as a tactic-level automation for HOL4: TacticToe. It implements a modified A*-algorithm directly in HOL4 that explores different tactic-level proof paths, guiding their selection by learning from a large number of previous tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids translation to FOL, working directly on the HOL level. By combining tactic prediction and premise selection, TacticToe is able to re-prove 39% of 7902 HOL4 theorems in 5 seconds whereas the best single HOL(y)Hammer strategy solves 32% in the same amount of time.

scholarly journals Challenge to the proving of theorems of Euclid's elements of as ATP

2019 ◽  
Vol 3 (4) ◽  
pp. 9-13
Author(s):  
Keyword(s):  
Mathematical Logic ◽  
Mathematics Education ◽  
Theorem Proving ◽  
Automated Reasoning ◽  
Automated Theorem Proving ◽  
Euclidean Geometry ◽  
Proof Assistant ◽  
Weak Point ◽  
Euclid’S Elements ◽  
Generic Proof

Automated theorem proving (ATP) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. An Isabelle/HOL is a generic proof assistant. We perform the challenge for the proving theorems of Euclid's elements of geometry. We could prove some theorems of Euclid's elements of geometry. Technique of programing and mental conception interact. The mathematics education which prove theorems of the Euclidean geometry by using the Isabelle/HOL can correct the present weak point

Introduction and Overview

2017 ◽  
Author(s):  
Neil Tennant
Keyword(s):  
Scientific Method ◽  
Proof Theory ◽  
Valid Argument ◽  
First Order ◽  
Proof Systems ◽  
Formal Systems ◽  
Deductive Logic ◽  
Order Language ◽  
Foundational Work ◽  
The Right

This is a foundational work, written not just for philosophers of logic, but for logicians and foundationalists generally. Like Frege we seek to deal with the formal first-order language of mathematics. We revisit Gentzen’s proof theory in order to build relevance into proofs, while leaving intact all the logical power one is entitled to expect of a deductive logic for mathematics and for scientific method generally. Proof systems are constituted by particular choices of rules of inference. We raise the issue of the reflexive stability of any argument for a particular choice of logic as the ‘right’ logic. We examine the question of pluralism v. absolutism in choice of logic, and suggest that the informal notion of valid argument is stable and robust enough for us to be able to ‘get it right’ with our formal systems of proof for both constructive and non-constructive reasoning.

A Test of ‘Utilitarianism for Animals, Kantianism for People’

2021 ◽  
pp. 1-27
Author(s):  
David Wendler
Keyword(s):  
Medical Research ◽  
Moral Status ◽  
Theoretical Basis ◽  
Common Belief ◽  
Human Beings ◽  
Robert Nozick ◽  
Side Constraints ◽  
The Common

Abstract Many people believe that animals possess moral status, but human beings possess higher moral status than animals. To provide a theoretical basis for this view, Robert Nozick proposed Utilitarianism for Animals, Kantianism for People. The present manuscript evaluates Nozick’s proposal by identifying the tradeoffs in welfare that it permits in medical research with animals and assessing whether those tradeoffs are indeed permissible. This analysis suggests that at least some deontological side constraints apply to the treatment of sentient animals, hence, Utilitarianism for Animals, Kantianism for People is mistaken. Because Nozick’s proposal represents a prominent attempt to provide a theoretical basis for the common belief that human beings possess higher moral status than animals, this conclusion is noteworthy in its own right. Moreover, by granting equal moral weight to the interests of animals, but reserving deontological side constraints for human beings, Utilitarianism for Animals, Kantianism for People offers one of the more plausible bases for the claim that there are degrees of moral status among those who matter morally. The manuscript thus ends by considering the implications of the present analysis for the possibility that moral status comes in degrees.

Gentzen's Proof Systems: Byproducts in a Work of Genius

2012 ◽  
Vol 18 (3) ◽  
pp. 313-367 ◽  
Author(s):  
Jan von Plato
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Central Component ◽  
Cut Elimination ◽  
Complete Class ◽  
Tree Form ◽  
Proof Systems ◽  
Set Up ◽  
Logical Calculi ◽  
Subformula Property

AbstractGentzen's systems of natural deduction and sequent calculus were byproducts in his program of proving the consistency of arithmetic and analysis. It is suggested that the central component in his results on logical calculi was the use of a tree form for derivations. It allows the composition of derivations and the permutation of the order of application of rules, with a full control over the structure of derivations as a result. Recently found documents shed new light on the discovery of these calculi. In particular, Gentzen set up five different forms of natural calculi and gave a detailed proof of normalization for intuitionistic natural deduction. An early handwritten manuscript of his thesis shows that a direct translation from natural deduction to the axiomatic logic of Hilbert and Ackermann was, in addition to the influence of Paul Hertz, the second component in the discovery of sequent calculus. A system intermediate between the sequent calculus LI and axiomatic logic, denoted LIG in unpublished sources, is implicit in Gentzen's published thesis of 1934–35. The calculus has half rules, half “groundsequents,” and does not allow full cut elimination. Nevertheless, a translation from LI to LIG in the published thesis gives a subformula property for a complete class of derivations in LIG. After the thesis, Gentzen continued to work on variants of sequent calculi for ten more years, in the hope to find a consistency proof for arithmetic within an intuitionistic calculus.

Sign in / Sign up

Export Citation Format

Share Document