Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-2020
Commits
a80f4e41ac2b
Commit
4d14c300
authored
Dec 22, 2020
by
Rene Thiemann
Browse files
sitegen and metadata
parent
85bc7487435c
Changes
6
Expand all
Hide whitespace changes
Inline
Side-by-side
metadata/metadata
View file @
a80f4e41
...
...
@@ -9964,3 +9964,21 @@ abstract =
We verify the correctness of Prim's, Kruskal's and
Borůvka's minimum spanning tree algorithms based on algebras for
aggregation and minimisation.
[Topological_Semantics]
title = Topological semantics for paraconsistent and paracomplete logics
author = David Fuenmayor <mailto:davfuenmayor@gmail.com>
topic = Logic/General logic
date = 2020-12-17
notify = davfuenmayor@gmail.com
abstract =
We introduce a generalized topological semantics for paraconsistent
and paracomplete logics by drawing upon early works on topological
Boolean algebras (cf. works by Kuratowski, Zarycki, McKinsey &
Tarski, etc.). In particular, this work exemplarily illustrates the
shallow semantical embeddings approach (<a
href="http://dx.doi.org/10.1007/s11787-012-0052-y">SSE</a>)
employing the proof assistant Isabelle/HOL. By means of the SSE
technique we can effectively harness theorem provers, model finders
and 'hammers' for reasoning with quantified non-classical
logics.
web/entries/Topological_Semantics.html
0 → 100644
View file @
a80f4e41
<!DOCTYPE html>
<html
lang=
"en"
>
<head>
<meta
charset=
"utf-8"
>
<title>
Topological semantics for paraconsistent and paracomplete logics - Archive of Formal Proofs
</title>
<link
rel=
"stylesheet"
type=
"text/css"
href=
"../front.css"
>
<link
rel=
"icon"
href=
"../images/favicon.ico"
type=
"image/icon"
>
<link
rel=
"alternate"
type=
"application/rss+xml"
title=
"RSS"
href=
"../rss.xml"
>
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax
=
{
tex
:
{
inlineMath
:
[[
'
$
'
,
'
$
'
],
[
'
\\
(
'
,
'
\\
)
'
]]
},
processEscapes
:
true
,
svg
:
{
fontCache
:
'
global
'
}
};
</script>
<script
id=
"MathJax-script"
async
src=
"../components/mathjax/es5/tex-mml-chtml.js"
></script>
</head>
<body
class=
"mathjax_ignore"
>
<table
width=
"100%"
>
<tbody>
<tr>
<!-- Navigation -->
<td
width=
"20%"
align=
"center"
valign=
"top"
>
<p>
</p>
<a
href=
"https://www.isa-afp.org/"
>
<img
src=
"../images/isabelle.png"
width=
"100"
height=
"88"
border=
0
>
</a>
<p>
</p>
<p>
</p>
<table
class=
"nav"
width=
"80%"
>
<tr>
<td
class=
"nav"
width=
"100%"
><a
href=
"../index.html"
>
Home
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../about.html"
>
About
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../submitting.html"
>
Submission
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../updating.html"
>
Updating Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../using.html"
>
Using Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../search.html"
>
Search
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../statistics.html"
>
Statistics
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../topics.html"
>
Index
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../download.html"
>
Download
</a></td>
</tr>
</table>
<p>
</p>
<p>
</p>
</td>
<!-- Content -->
<td
width=
"80%"
valign=
"top"
>
<div
align=
"center"
>
<p>
</p>
<h1>
<font
class=
"first"
>
T
</font>
opological
semantics
for
paraconsistent
and
paracomplete
logics
</h1>
<p>
</p>
<table
width=
"80%"
class=
"data"
>
<tbody>
<tr>
<td
class=
"datahead"
width=
"20%"
>
Title:
</td>
<td
class=
"data"
width=
"80%"
>
Topological semantics for paraconsistent and paracomplete logics
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Author:
</td>
<td
class=
"data"
>
David Fuenmayor (davfuenmayor /at/ gmail /dot/ com)
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Submission date:
</td>
<td
class=
"data"
>
2020-12-17
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
Abstract:
</td>
<td
class=
"abstract mathjax_process"
>
We introduce a generalized topological semantics for paraconsistent
and paracomplete logics by drawing upon early works on topological
Boolean algebras (cf. works by Kuratowski, Zarycki, McKinsey
&
Tarski, etc.). In particular, this work exemplarily illustrates the
shallow semantical embeddings approach (
<a
href=
"http://dx.doi.org/10.1007/s11787-012-0052-y"
>
SSE
</a>
)
employing the proof assistant Isabelle/HOL. By means of the SSE
technique we can effectively harness theorem provers, model finders
and 'hammers' for reasoning with quantified non-classical
logics.
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
BibTeX:
</td>
<td
class=
"formatted"
>
<pre>
@article{Topological_Semantics-AFP,
author = {David Fuenmayor},
title = {Topological semantics for paraconsistent and paracomplete logics},
journal = {Archive of Formal Proofs},
month = dec,
year = 2020,
note = {\url{https://isa-afp.org/entries/Topological_Semantics.html},
Formal proof development},
ISSN = {2150-914x},
}
</pre>
</td>
</tr>
<tr><td
class=
"datahead"
>
License:
</td>
<td
class=
"data"
><a
href=
"http://isa-afp.org/LICENSE"
>
BSD License
</a></td></tr>
</tbody>
</table>
<p></p>
<table
class=
"links"
>
<tbody>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Topological_Semantics/outline.pdf"
>
Proof outline
</a><br>
<a
href=
"../browser_info/current/AFP/Topological_Semantics/document.pdf"
>
Proof document
</a>
</td>
</tr>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Topological_Semantics/index.html"
>
Browse theories
</a>
</td></tr>
<tr>
<td
class=
"links"
>
<a
href=
"../release/afp-Topological_Semantics-current.tar.gz"
>
Download this entry
</a>
</td>
</tr>
<tr><td
class=
"links"
>
Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script
src=
"../jquery.min.js"
></script>
<script
src=
"../script.js"
></script>
</body>
</html>
\ No newline at end of file
web/index.html
View file @
a80f4e41
...
...
@@ -88,6 +88,14 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<tr>
<td
class=
"head"
>
2020
</td>
</tr>
<tr>
<td
class=
"entry"
>
2020-12-17:
<a
href=
"entries/Topological_Semantics.html"
>
Topological semantics for paraconsistent and paracomplete logics
</a>
<br>
Author:
David Fuenmayor
</td>
</tr>
<tr>
<td
class=
"entry"
>
2020-12-08:
<a
href=
"entries/Relational_Minimum_Spanning_Trees.html"
>
Relational Minimum Spanning Tree Algorithms
</a>
...
...
web/rss.xml
View file @
a80f4e41
...
...
@@ -9,7 +9,25 @@
and larger scientific developments, mechanically checked
in the theorem prover Isabelle.
</description>
<pubDate>
08 Dec 2020 00:00:00 +0000
</pubDate>
<pubDate>
17 Dec 2020 00:00:00 +0000
</pubDate>
<item>
<title>
Topological semantics for paraconsistent and paracomplete logics
</title>
<link>
https://www.isa-afp.org/entries/Topological_Semantics.html
</link>
<guid>
https://www.isa-afp.org/entries/Topological_Semantics.html
</guid>
<dc:creator>
David Fuenmayor
</dc:creator>
<pubDate>
17 Dec 2020 00:00:00 +0000
</pubDate>
<description>
We introduce a generalized topological semantics for paraconsistent
and paracomplete logics by drawing upon early works on topological
Boolean algebras (cf. works by Kuratowski, Zarycki, McKinsey
&
Tarski, etc.). In particular, this work exemplarily illustrates the
shallow semantical embeddings approach (
<
a
href=
"
http://dx.doi.org/10.1007/s11787-012-0052-y
">
SSE
<
/a
>
)
employing the proof assistant Isabelle/HOL. By means of the SSE
technique we can effectively harness theorem provers, model finders
and
'
hammers
'
for reasoning with quantified non-classical
logics.
</description>
</item>
<item>
<title>
Relational Minimum Spanning Tree Algorithms
</title>
<link>
https://www.isa-afp.org/entries/Relational_Minimum_Spanning_Trees.html
</link>
...
...
@@ -574,20 +592,5 @@ several properties such as strong normalization, the subterm property,
closure properties under substitutions and contexts, as well as ground
totality.
</description>
</item>
<item>
<title>
Irrationality Criteria for Series by Erdős and Straus
</title>
<link>
https://www.isa-afp.org/entries/Irrational_Series_Erdos_Straus.html
</link>
<guid>
https://www.isa-afp.org/entries/Irrational_Series_Erdos_Straus.html
</guid>
<dc:creator>
Angeliki Koutsoukou-Argyraki, Wenda Li
</dc:creator>
<pubDate>
12 May 2020 00:00:00 +0000
</pubDate>
<description>
We formalise certain irrationality criteria for infinite series of the form:
\[\sum_{n=1}^\infty \frac{b_n}{\prod_{i=1}^n a_i} \]
where $\{b_n\}$ is a sequence of integers and $\{a_n\}$ a sequence of positive integers
with $a_n
>
1$ for all large n. The results are due to P. Erdős and E. G. Straus
<
a href=
"
https://projecteuclid.org/euclid.pjm/1102911140
">
[1]
<
/a
>
.
In particular, we formalise Theorem 2.1, Corollary 2.10 and Theorem 3.1.
The latter is an application of Theorem 2.1 involving the prime numbers.
</description>
</item>
</channel>
</rss>
web/statistics.html
View file @
a80f4e41
This diff is collapsed.
Click to expand it.
web/topics.html
View file @
a80f4e41
...
...
@@ -515,6 +515,7 @@
</div>
<h3>
General logic
</h3>
<div
class=
"list"
>
<a
href=
"entries/Topological_Semantics.html"
>
Topological_Semantics
</a>
<strong>
Classical propositional logic:
</strong>
<a
href=
"entries/Free-Boolean-Algebra.html"
>
Free-Boolean-Algebra
</a>
<strong>
Classical first-order logic:
</strong>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment