Detection of First Order Axiomatic Theories
Identifieur interne : 001601 ( Main/Exploration ); précédent : 001600; suivant : 001602Detection of First Order Axiomatic Theories
Auteurs : Guillaume Burel [France] ; Simon Cruanes [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Automated theorem provers for first-order logic with equality have become very powerful and useful, thanks to both advanced calculi — such as superposition and its refinements — and mature implementation techniques. Nevertheless, dealing with some axiomatic theories remains a challenge because it gives rise to a search space explosion. Most attempts to deal with this problem have focused on specific theories, like AC (associative commutative symbols) or ACU (AC with neutral element). Even detecting the presence of a theory in a problem is generally solved in an ad-hoc fashion. We present here a generic way of describing and recognizing axiomatic theories in clausal form first-order logic with equality. Subsequently, we show some use cases for it, including a redundancy criterion that can be applied to some equational theories, extending some work that has been done by Avenhaus, Hillenbrand and Löchner.
Url:
DOI: 10.1007/978-3-642-40885-4_16
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001927
- to stream Istex, to step Curation: 001908
- to stream Istex, to step Checkpoint: 000227
- to stream Main, to step Merge: 001613
- to stream Main, to step Curation: 001601
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Detection of First Order Axiomatic Theories</title><author><name sortKey="Burel, Guillaume" sort="Burel, Guillaume" uniqKey="Burel G" first="Guillaume" last="Burel">Guillaume Burel</name></author><author><name sortKey="Cruanes, Simon" sort="Cruanes, Simon" uniqKey="Cruanes S" first="Simon" last="Cruanes">Simon Cruanes</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:6C7ED2C16DE343366D5B18E118F85D27D822FAD6</idno><date when="2013" year="2013">2013</date><idno type="doi">10.1007/978-3-642-40885-4_16</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-5HW5WDF2-7/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001927</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001927</idno><idno type="wicri:Area/Istex/Curation">001908</idno><idno type="wicri:Area/Istex/Checkpoint">000227</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000227</idno><idno type="wicri:doubleKey">0302-9743:2013:Burel G:detection:of:first</idno><idno type="wicri:Area/Main/Merge">001613</idno><idno type="wicri:Area/Main/Curation">001601</idno><idno type="wicri:Area/Main/Exploration">001601</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Detection of First Order Axiomatic Theories</title><author><name sortKey="Burel, Guillaume" sort="Burel, Guillaume" uniqKey="Burel G" first="Guillaume" last="Burel">Guillaume Burel</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>ÉNSIIE/Cédric, 1 square de la résistance, 91025, Évry cedex</wicri:regionArea><placeName><region type="region" nuts="2">Île-de-France</region><settlement type="city">Évry (Essonne)</settlement></placeName></affiliation></author><author><name sortKey="Cruanes, Simon" sort="Cruanes, Simon" uniqKey="Cruanes S" first="Simon" last="Cruanes">Simon Cruanes</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>École polytechnique and INRIA, 23 Avenue d’Italie, 75013, Paris</wicri:regionArea><placeName><region type="region" nuts="2">Île-de-France</region><settlement type="city">Paris</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Automated theorem provers for first-order logic with equality have become very powerful and useful, thanks to both advanced calculi — such as superposition and its refinements — and mature implementation techniques. Nevertheless, dealing with some axiomatic theories remains a challenge because it gives rise to a search space explosion. Most attempts to deal with this problem have focused on specific theories, like AC (associative commutative symbols) or ACU (AC with neutral element). Even detecting the presence of a theory in a problem is generally solved in an ad-hoc fashion. We present here a generic way of describing and recognizing axiomatic theories in clausal form first-order logic with equality. Subsequently, we show some use cases for it, including a redundancy criterion that can be applied to some equational theories, extending some work that has been done by Avenhaus, Hillenbrand and Löchner.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Île-de-France</li></region><settlement><li>Paris</li><li>Évry (Essonne)</li></settlement></list><tree><country name="France"><region name="Île-de-France"><name sortKey="Burel, Guillaume" sort="Burel, Guillaume" uniqKey="Burel G" first="Guillaume" last="Burel">Guillaume Burel</name></region><name sortKey="Cruanes, Simon" sort="Cruanes, Simon" uniqKey="Cruanes S" first="Simon" last="Cruanes">Simon Cruanes</name><name sortKey="Cruanes, Simon" sort="Cruanes, Simon" uniqKey="Cruanes S" first="Simon" last="Cruanes">Simon Cruanes</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001601 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001601 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:6C7ED2C16DE343366D5B18E118F85D27D822FAD6
|texte= Detection of First Order Axiomatic Theories
}}
| This area was generated with Dilib version V0.6.33. |  |