Proof-search in intuitionistic logic based on constraint satisfaction

1996 ◽  
pp. 312-329 ◽  
Author(s):  
Andrei Voronkov
Keyword(s):  
Intuitionistic Logic ◽  
Constraint Satisfaction ◽  
Proof Search

scholarly journals Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus

2008 ◽  
Vol 48 ◽  
Author(s):  
Romas Alonderis
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Sequent Calculus ◽  
Proof Search

In the paper, we define some classes of sequents of the propositional intuitionistic logic. These are classes of primarily and α-primarily reducible sequents. Then we show how derivability of these sequents in a propositional intuitionistic logic sequent calculus LJ0 can be checked by means of a propositional classical logic sequent calculus LK0.

Intuitionistic logic freed of all metarules

2007 ◽  
Vol 72 (4) ◽  
pp. 1204-1218 ◽  
Author(s):  
Giovanna Corsi ◽  
Gabriele Tassi
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Proof Search ◽  
Subformula Property

AbstractIn this paper we present two calculi for intuitionistic logic. The first one. IG, is characterized by the fact that every proof-search terminates and termination is reached without jeopardizing the subformula property. As to the second one, SIC, proof-search terminates, the subformula property is preserved and moreover proof-search is performed without any recourse to metarules, in particular there is no need to back-track. As a consequence, proof-search in the calculus SIC is accomplished by a single tree as in classical logic.

scholarly journals First-order Answer Set Programming as Constructive Proof Search

2018 ◽  
Vol 18 (3-4) ◽  
pp. 673-690
Author(s):  
ALEKSY SCHUBERT ◽  
PAWEŁ URZYCZYN
Keyword(s):  
Logic Programming ◽  
Intuitionistic Logic ◽  
Proof Theory ◽  
Answer Set Programming ◽  
Theory And Practice ◽  
Close Similarity ◽  
Constructive Proof ◽  
First Order ◽  
Proof Search ◽  
Answer Set

AbstractWe propose an interpretation of the first-order answer set programming (FOASP) in terms of intuitionistic proof theory. It is obtained by two polynomial translations between FOASP and the bounded-arity fragment of the Σ1 level of the Mints hierarchy in first-order intuitionistic logic. It follows that Σ1 formulas using predicates of fixed arity (in particular unary) is of the same strength as FOASP. Our construction reveals a close similarity between constructive provability and stable entailment, or equivalently, between the construction of an answer set and an intuitionistic refutation. This paper is under consideration for publication in Theory and Practice of Logic Programming

scholarly journals Dialogues for proof search

10.29007/5t86 ◽  
2018 ◽  
Author(s):  
Jesse Alama
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Order Logic ◽  
Theorem Prover ◽  
First Order Logic ◽  
Dialogue Games ◽  
First Order ◽  
Proof Search ◽  
Automated Theorem Prover

Dialogue games are a two-player semantics for a variety of logics, including intuitionistic and classical logic. Dialogues can be viewed as a kind of analytic calculus not unlike tableaux. Can dialogue games be an effective foundation for proof search in intuitionistic logic (both first-order and propositional)? We announce Kuno, an automated theorem prover for intuitionistic first-order logic based on dialogue games.

Sign in / Sign up

Export Citation Format

Share Document