On the intuitionistic force of classical search
Identifieur interne : 000A75 ( PascalFrancis/Corpus ); précédent : 000A74; suivant : 000A76On the intuitionistic force of classical search
Auteurs : E. Ritter ; D. Pym ; L. WallenSource :
- Theoretical computer science [ 0304-3975 ] ; 2000.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
The combinatorics of classical propositional logic lies at the heart of both local and global methods of proof-search enabling the achievement of least-commitment search. Extension of such methods to the predicate calculus, or to non-classical systems, presents us with the problem of recovering this least-commitment principle in the context of non-invertible rules. One successful approach is to view the non-classical logic as a perturbation on search in classical logic and characterize when a least-commitment (classical) search yields sufficient evidence for provability in the (non-classical) logic. This technique has been successfully applied to both local and global methods at the cost of subsidiary searches and is the analogue of the standard treatment of quantifiers via skolemization and unification. In this paper, we take a type-theoretic view of this approach for the case in which the non-classical logic is intuitionistic. We develop a system of realizers (proof-objects) for sequents in classical propositional logic (the types) by extending Parigot's λμ-calculus, a system of realizers for classical free deduction (cf. natural deduction). Our treatment of disjunction exploits directly the multiple-conclusioned form of LK as opposed to the single-conclusioned form of LJ. Consequently, it requires the addition of another binding operator, called v, to λμ. This choice is motivated by our concern to reflect the properties of classical proof-search in the system of realizers. Using this framework, we illustrate the sense in which intuitionistic search can be viewed as a perturbation on classical search. As an application, we develop a proof procedure based on the natural extension of the notion of uniform proof to the multiple-conclusioned classical sequent calculus Harrop fragment of intuitionistic logic. This paper develops the proof-theoretic aspects of the approach.
Notice en format standard (ISO 2709)
Pour connaître la documentation sur le format Inist Standard.
pA |
|
---|
Format Inist (serveur)
NO : | PASCAL 00-0103172 INIST |
---|---|
ET : | On the intuitionistic force of classical search |
AU : | RITTER (E.); PYM (D.); WALLEN (L.); GALMICHE (Didier); PYM (David J.) |
AF : | School of Computer Science, University of Birmingham/Birmingham, B15 2TT/Royaume-Uni (1 aut.); Department of Computer Science, Queen Mary & Westfield College, University of London. Mile End Road/London, E1 4NS/Royaume-Uni (2 aut.); Programming Research Group, Computing Laboratory, Oxford University, 8-11 Keble Road/Oxford, OX1 3QD/Royaume-Uni (3 aut.); LORIA - Université Henri Poincaré, Campus Scientifique, B.P. 239/54506 Vandoeuvre-les-Nancy/France (1 aut.); Queen Mary & Westfield College, Department of Computer Science, University of London, Mile End Road/London, E1 4NS/Royaume-Uni (2 aut.) |
DT : | Publication en série; Niveau analytique |
SO : | Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 2000; Vol. 232; No. 1-2; Pp. 299-333; Bibl. 35 ref. |
LA : | Anglais |
EA : | The combinatorics of classical propositional logic lies at the heart of both local and global methods of proof-search enabling the achievement of least-commitment search. Extension of such methods to the predicate calculus, or to non-classical systems, presents us with the problem of recovering this least-commitment principle in the context of non-invertible rules. One successful approach is to view the non-classical logic as a perturbation on search in classical logic and characterize when a least-commitment (classical) search yields sufficient evidence for provability in the (non-classical) logic. This technique has been successfully applied to both local and global methods at the cost of subsidiary searches and is the analogue of the standard treatment of quantifiers via skolemization and unification. In this paper, we take a type-theoretic view of this approach for the case in which the non-classical logic is intuitionistic. We develop a system of realizers (proof-objects) for sequents in classical propositional logic (the types) by extending Parigot's λμ-calculus, a system of realizers for classical free deduction (cf. natural deduction). Our treatment of disjunction exploits directly the multiple-conclusioned form of LK as opposed to the single-conclusioned form of LJ. Consequently, it requires the addition of another binding operator, called v, to λμ. This choice is motivated by our concern to reflect the properties of classical proof-search in the system of realizers. Using this framework, we illustrate the sense in which intuitionistic search can be viewed as a perturbation on classical search. As an application, we develop a proof procedure based on the natural extension of the notion of uniform proof to the multiple-conclusioned classical sequent calculus Harrop fragment of intuitionistic logic. This paper develops the proof-theoretic aspects of the approach. |
CC : | 001A02A01F; 001A02A01B |
FD : | Logique; Programmation logique; Lambda calcul; Substitution; Recherche preuve; Calcul lambda mu; Logique intuitionniste; Preuve uniforme |
ED : | Logic; Logical programming; Lambda calculus; Substitution; Proof search; Lambda mu calculus; Intuitionistic logic; Uniform proof |
SD : | Lógica; Programación lógica; Lambda cálculo; Substitución |
LO : | INIST-17243.354000081470930100 |
ID : | 00-0103172 |
Links to Exploration step
Pascal:00-0103172Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">On the intuitionistic force of classical search</title>
<author><name sortKey="Ritter, E" sort="Ritter, E" uniqKey="Ritter E" first="E." last="Ritter">E. Ritter</name>
<affiliation><inist:fA14 i1="01"><s1>School of Computer Science, University of Birmingham</s1>
<s2>Birmingham, B15 2TT</s2>
<s3>GBR</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Pym, D" sort="Pym, D" uniqKey="Pym D" first="D." last="Pym">D. Pym</name>
<affiliation><inist:fA14 i1="02"><s1>Department of Computer Science, Queen Mary & Westfield College, University of London. Mile End Road</s1>
<s2>London, E1 4NS</s2>
<s3>GBR</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Wallen, L" sort="Wallen, L" uniqKey="Wallen L" first="L." last="Wallen">L. Wallen</name>
<affiliation><inist:fA14 i1="03"><s1>Programming Research Group, Computing Laboratory, Oxford University, 8-11 Keble Road</s1>
<s2>Oxford, OX1 3QD</s2>
<s3>GBR</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">00-0103172</idno>
<date when="2000">2000</date>
<idno type="stanalyst">PASCAL 00-0103172 INIST</idno>
<idno type="RBID">Pascal:00-0103172</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000A75</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">On the intuitionistic force of classical search</title>
<author><name sortKey="Ritter, E" sort="Ritter, E" uniqKey="Ritter E" first="E." last="Ritter">E. Ritter</name>
<affiliation><inist:fA14 i1="01"><s1>School of Computer Science, University of Birmingham</s1>
<s2>Birmingham, B15 2TT</s2>
<s3>GBR</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Pym, D" sort="Pym, D" uniqKey="Pym D" first="D." last="Pym">D. Pym</name>
<affiliation><inist:fA14 i1="02"><s1>Department of Computer Science, Queen Mary & Westfield College, University of London. Mile End Road</s1>
<s2>London, E1 4NS</s2>
<s3>GBR</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Wallen, L" sort="Wallen, L" uniqKey="Wallen L" first="L." last="Wallen">L. Wallen</name>
<affiliation><inist:fA14 i1="03"><s1>Programming Research Group, Computing Laboratory, Oxford University, 8-11 Keble Road</s1>
<s2>Oxford, OX1 3QD</s2>
<s3>GBR</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
<imprint><date when="2000">2000</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Intuitionistic logic</term>
<term>Lambda calculus</term>
<term>Lambda mu calculus</term>
<term>Logic</term>
<term>Logical programming</term>
<term>Proof search</term>
<term>Substitution</term>
<term>Uniform proof</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Logique</term>
<term>Programmation logique</term>
<term>Lambda calcul</term>
<term>Substitution</term>
<term>Recherche preuve</term>
<term>Calcul lambda mu</term>
<term>Logique intuitionniste</term>
<term>Preuve uniforme</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">The combinatorics of classical propositional logic lies at the heart of both local and global methods of proof-search enabling the achievement of least-commitment search. Extension of such methods to the predicate calculus, or to non-classical systems, presents us with the problem of recovering this least-commitment principle in the context of non-invertible rules. One successful approach is to view the non-classical logic as a perturbation on search in classical logic and characterize when a least-commitment (classical) search yields sufficient evidence for provability in the (non-classical) logic. This technique has been successfully applied to both local and global methods at the cost of subsidiary searches and is the analogue of the standard treatment of quantifiers via skolemization and unification. In this paper, we take a type-theoretic view of this approach for the case in which the non-classical logic is intuitionistic. We develop a system of realizers (proof-objects) for sequents in classical propositional logic (the types) by extending Parigot's λμ-calculus, a system of realizers for classical free deduction (cf. natural deduction). Our treatment of disjunction exploits directly the multiple-conclusioned form of LK as opposed to the single-conclusioned form of LJ. Consequently, it requires the addition of another binding operator, called v, to λμ. This choice is motivated by our concern to reflect the properties of classical proof-search in the system of realizers. Using this framework, we illustrate the sense in which intuitionistic search can be viewed as a perturbation on classical search. As an application, we develop a proof procedure based on the natural extension of the notion of uniform proof to the multiple-conclusioned classical sequent calculus Harrop fragment of intuitionistic logic. This paper develops the proof-theoretic aspects of the approach.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0304-3975</s0>
</fA01>
<fA02 i1="01"><s0>TCSCDI</s0>
</fA02>
<fA03 i2="1"><s0>Theor. comput. sci.</s0>
</fA03>
<fA05><s2>232</s2>
</fA05>
<fA06><s2>1-2</s2>
</fA06>
<fA08 i1="01" i2="1" l="ENG"><s1>On the intuitionistic force of classical search</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>Proof-search in Type-theoretic Languages</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>RITTER (E.)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>PYM (D.)</s1>
</fA11>
<fA11 i1="03" i2="1"><s1>WALLEN (L.)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>GALMICHE (Didier)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="02" i2="1"><s1>PYM (David J.)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01"><s1>School of Computer Science, University of Birmingham</s1>
<s2>Birmingham, B15 2TT</s2>
<s3>GBR</s3>
<sZ>1 aut.</sZ>
</fA14>
<fA14 i1="02"><s1>Department of Computer Science, Queen Mary & Westfield College, University of London. Mile End Road</s1>
<s2>London, E1 4NS</s2>
<s3>GBR</s3>
<sZ>2 aut.</sZ>
</fA14>
<fA14 i1="03"><s1>Programming Research Group, Computing Laboratory, Oxford University, 8-11 Keble Road</s1>
<s2>Oxford, OX1 3QD</s2>
<s3>GBR</s3>
<sZ>3 aut.</sZ>
</fA14>
<fA15 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique, B.P. 239</s1>
<s2>54506 Vandoeuvre-les-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA15>
<fA15 i1="02"><s1>Queen Mary & Westfield College, Department of Computer Science, University of London, Mile End Road</s1>
<s2>London, E1 4NS</s2>
<s3>GBR</s3>
<sZ>2 aut.</sZ>
</fA15>
<fA20><s1>299-333</s1>
</fA20>
<fA21><s1>2000</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA43 i1="01"><s1>INIST</s1>
<s2>17243</s2>
<s5>354000081470930100</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2000 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>35 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>00-0103172</s0>
</fA47>
<fA60><s1>P</s1>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>Theoretical computer science</s0>
</fA64>
<fA66 i1="01"><s0>NLD</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>The combinatorics of classical propositional logic lies at the heart of both local and global methods of proof-search enabling the achievement of least-commitment search. Extension of such methods to the predicate calculus, or to non-classical systems, presents us with the problem of recovering this least-commitment principle in the context of non-invertible rules. One successful approach is to view the non-classical logic as a perturbation on search in classical logic and characterize when a least-commitment (classical) search yields sufficient evidence for provability in the (non-classical) logic. This technique has been successfully applied to both local and global methods at the cost of subsidiary searches and is the analogue of the standard treatment of quantifiers via skolemization and unification. In this paper, we take a type-theoretic view of this approach for the case in which the non-classical logic is intuitionistic. We develop a system of realizers (proof-objects) for sequents in classical propositional logic (the types) by extending Parigot's λμ-calculus, a system of realizers for classical free deduction (cf. natural deduction). Our treatment of disjunction exploits directly the multiple-conclusioned form of LK as opposed to the single-conclusioned form of LJ. Consequently, it requires the addition of another binding operator, called v, to λμ. This choice is motivated by our concern to reflect the properties of classical proof-search in the system of realizers. Using this framework, we illustrate the sense in which intuitionistic search can be viewed as a perturbation on classical search. As an application, we develop a proof procedure based on the natural extension of the notion of uniform proof to the multiple-conclusioned classical sequent calculus Harrop fragment of intuitionistic logic. This paper develops the proof-theoretic aspects of the approach.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001A02A01F</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001A02A01B</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Logique</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Logic</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Lógica</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Programmation logique</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Logical programming</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Programación lógica</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Lambda calcul</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Lambda calculus</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Lambda cálculo</s0>
<s5>03</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Substitution</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Substitution</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Substitución</s0>
<s5>04</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Recherche preuve</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Proof search</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Calcul lambda mu</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Lambda mu calculus</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Logique intuitionniste</s0>
<s4>CD</s4>
<s5>98</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Intuitionistic logic</s0>
<s4>CD</s4>
<s5>98</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Preuve uniforme</s0>
<s4>CD</s4>
<s5>99</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Uniform proof</s0>
<s4>CD</s4>
<s5>99</s5>
</fC03>
<fN21><s1>073</s1>
</fN21>
</pA>
</standard>
<server><NO>PASCAL 00-0103172 INIST</NO>
<ET>On the intuitionistic force of classical search</ET>
<AU>RITTER (E.); PYM (D.); WALLEN (L.); GALMICHE (Didier); PYM (David J.)</AU>
<AF>School of Computer Science, University of Birmingham/Birmingham, B15 2TT/Royaume-Uni (1 aut.); Department of Computer Science, Queen Mary & Westfield College, University of London. Mile End Road/London, E1 4NS/Royaume-Uni (2 aut.); Programming Research Group, Computing Laboratory, Oxford University, 8-11 Keble Road/Oxford, OX1 3QD/Royaume-Uni (3 aut.); LORIA - Université Henri Poincaré, Campus Scientifique, B.P. 239/54506 Vandoeuvre-les-Nancy/France (1 aut.); Queen Mary & Westfield College, Department of Computer Science, University of London, Mile End Road/London, E1 4NS/Royaume-Uni (2 aut.)</AF>
<DT>Publication en série; Niveau analytique</DT>
<SO>Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 2000; Vol. 232; No. 1-2; Pp. 299-333; Bibl. 35 ref.</SO>
<LA>Anglais</LA>
<EA>The combinatorics of classical propositional logic lies at the heart of both local and global methods of proof-search enabling the achievement of least-commitment search. Extension of such methods to the predicate calculus, or to non-classical systems, presents us with the problem of recovering this least-commitment principle in the context of non-invertible rules. One successful approach is to view the non-classical logic as a perturbation on search in classical logic and characterize when a least-commitment (classical) search yields sufficient evidence for provability in the (non-classical) logic. This technique has been successfully applied to both local and global methods at the cost of subsidiary searches and is the analogue of the standard treatment of quantifiers via skolemization and unification. In this paper, we take a type-theoretic view of this approach for the case in which the non-classical logic is intuitionistic. We develop a system of realizers (proof-objects) for sequents in classical propositional logic (the types) by extending Parigot's λμ-calculus, a system of realizers for classical free deduction (cf. natural deduction). Our treatment of disjunction exploits directly the multiple-conclusioned form of LK as opposed to the single-conclusioned form of LJ. Consequently, it requires the addition of another binding operator, called v, to λμ. This choice is motivated by our concern to reflect the properties of classical proof-search in the system of realizers. Using this framework, we illustrate the sense in which intuitionistic search can be viewed as a perturbation on classical search. As an application, we develop a proof procedure based on the natural extension of the notion of uniform proof to the multiple-conclusioned classical sequent calculus Harrop fragment of intuitionistic logic. This paper develops the proof-theoretic aspects of the approach.</EA>
<CC>001A02A01F; 001A02A01B</CC>
<FD>Logique; Programmation logique; Lambda calcul; Substitution; Recherche preuve; Calcul lambda mu; Logique intuitionniste; Preuve uniforme</FD>
<ED>Logic; Logical programming; Lambda calculus; Substitution; Proof search; Lambda mu calculus; Intuitionistic logic; Uniform proof</ED>
<SD>Lógica; Programación lógica; Lambda cálculo; Substitución</SD>
<LO>INIST-17243.354000081470930100</LO>
<ID>00-0103172</ID>
</server>
</inist>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000A75 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000A75 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= PascalFrancis |étape= Corpus |type= RBID |clé= Pascal:00-0103172 |texte= On the intuitionistic force of classical search }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |