Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
Alethe
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Iterations
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Locked files
Build
Pipelines
Jobs
Pipeline schedules
Test cases
Artifacts
Deploy
Releases
Model registry
Analyze
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Admin message
Pour rappel, le service sera inaccessible ce lundi 05/05/25 midi pour raison de mise à jour.
Show more breadcrumbs
veriT
Alethe
Commits
b4032d3f
Commit
b4032d3f
authored
2 years ago
by
Hans-Jörg
Browse files
Options
Downloads
Patches
Plain Diff
Add 0.3 description to changelog
parent
dc5a9659
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Pipeline
#10868
passed
2 years ago
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
spec/changelog.tex
+28
-0
28 additions, 0 deletions
spec/changelog.tex
with
28 additions
and
0 deletions
spec/changelog.tex
+
28
−
0
View file @
b4032d3f
\subsection*
{
0.3 --- Unreleased
}
This release overhauls the entire document, but introduces only few
changes to the proof format itself.
The standard now specifies that
\texttt
{
assume
}
commands can only be
issued at the start of the proof or right after an
\texttt
{
anchor
}
command.
Beyond many smaller clarifications and typographic improvments, the
following changes were implemented in this release.
\begin{itemize}
\item
An abstract proof checking procedure to clarify
the semantic of the proof format was added.
\item
A description of the semantic of contexts based on λ-terms
was added.
\item
The document now lists all transformations that are
implicit in Alethe proofs.
\item
The notation used for terms from first-order style
(e.g.,
$
f
(
x,g
(
y
))
$
) was changed to higher-order style (e.g.,
$
(
f
\;
x
\;
(
g
\;
y
))
$
). This only a change in notation -- the used logic
remains many-sorted first-order logic.
\item
The is no longer a distinction between if-and-only-if and
equaltiy. Instead equality (the symbol
$
≈
$
) is used with appropiate
sorts.
\item
An index that lists all proof rules was added.
\end{itemize}
\subsection*
{
0.2 ---
\DTMdisplaydate
{
2022
}{
12
}{
19
}{
-1
}}
This is an intermediate release. It collects all changes to the original
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment